Theorem mpanl1 424

Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpanl1.1	⊢ 𝜑
mpanl1.2	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mpanl1	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem mpanl1

Step	Hyp	Ref	Expression
1		mpanl1.1	. . 3 ⊢ 𝜑
2	1	jctl 307	. 2 ⊢ (𝜓 → (𝜑 ∧ 𝜓))
3		mpanl1.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	sylan 277	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  mpanl12  426  ercnv  6150  rec11api  7841  divdiv23apzi  7853  recp1lt1  7977  divgt0i  7988  divge0i  7989  ltreci  7990  lereci  7991  lt2msqi  7992  le2msqi  7993  msq11i  7994  ltdiv23i  8004  fnn0ind  8463  elfzp1b  9114  elfzm1b  9115  sqrt11i  10018  sqrtmuli  10019  sqrtmsq2i  10021  sqrtlei  10022  sqrtlti  10023