Theorem mpanl1 438

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  mpanl12  440  ercnv  6822  rec11api  9077  divdiv23apzi  9089  recp1lt1  9223  divgt0i  9234  divge0i  9235  ltreci  9236  lereci  9237  lt2msqi  9238  le2msqi  9239  msq11i  9240  ltdiv23i  9250  fnn0ind  9745  elfzp1b  10487  elfzm1b  10488  sqrt11i  11881  sqrtmuli  11882  sqrtmsq2i  11884  sqrtlei  11885  sqrtlti  11886