Theorem mpanl12 426

Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)

Hypotheses

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

Assertion

Ref	Expression
mpanl12	⊢ (𝜒 → 𝜃)

Proof of Theorem mpanl12

Step	Hyp	Ref	Expression
1		mpanl12.2	. 2 ⊢ 𝜓
2		mpanl12.1	. . 3 ⊢ 𝜑
3		mpanl12.3	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	mpanl1 424	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 414	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:  reuun1  3246  ordtri2orexmid  4266  opthreg  4299  ordtri2or2exmid  4314  fvtp1  5393  nq0m0r  6646  nq02m  6655  gt0srpr  6925  pitoregt0  7017  axcnre  7047  addgt0  7552  addgegt0  7553  addgtge0  7554  addge0  7555  addgt0i  7589  addge0i  7590  addgegt0i  7591  add20i  7593  mulge0i  7720  recextlem1  7741  recap0  7773  recdivap  7806  recgt1  7975  prodgt0i  7986  prodge0i  7987  iccshftri  9017  iccshftli  9019  iccdili  9021  icccntri  9023  mulexpzap  9516  expaddzap  9520  m1expeven  9523  iexpcyc  9579  amgm2  10004  sqnprm  10517