Theorem mpanl1 431

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 312	. 2 ⊢ (𝜓 → (𝜑 ∧ 𝜓))
3		mpanl1.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	sylan 281	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  mpanl12  433  ercnv  6458  rec11api  8537  divdiv23apzi  8549  recp1lt1  8681  divgt0i  8692  divge0i  8693  ltreci  8694  lereci  8695  lt2msqi  8696  le2msqi  8697  msq11i  8698  ltdiv23i  8708  fnn0ind  9191  elfzp1b  9908  elfzm1b  9909  sqrt11i  10936  sqrtmuli  10937  sqrtmsq2i  10939  sqrtlei  10940  sqrtlti  10941