Theorem mpanl12 428

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 426	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 416	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  reuun1  3297  ordtri2orexmid  4367  opthreg  4400  ordtri2or2exmid  4415  fvtp1  5547  nq0m0r  7112  nq02m  7121  gt0srpr  7391  pitoregt0  7483  axcnre  7513  addgt0  8023  addgegt0  8024  addgtge0  8025  addge0  8026  addgt0i  8063  addge0i  8064  addgegt0i  8065  add20i  8067  mulge0i  8194  recextlem1  8217  recap0  8249  recdivap  8282  recgt1  8455  prodgt0i  8466  prodge0i  8467  iccshftri  9561  iccshftli  9563  iccdili  9565  icccntri  9567  mulexpzap  10126  expaddzap  10130  m1expeven  10133  iexpcyc  10190  amgm2  10682  ege2le3  11126  sqnprm  11560  lmres  12115