Theorem mpanl12 440

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 438	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 428	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:  reuun1  3515  ordtri2orexmid  4668  opthreg  4701  ordtri2or2exmid  4716  ontri2orexmidim  4717  fvtp1  5920  nq0m0r  7817  nq02m  7826  gt0srpr  8109  map2psrprg  8166  pitoregt0  8210  axcnre  8242  addgt0  8770  addgegt0  8771  addgtge0  8772  addge0  8773  addgt0i  8810  addge0i  8811  addgegt0i  8812  add20i  8814  mulge0i  8942  recextlem1  8973  recap0  9009  recdivap  9042  recgt1  9221  prodgt0i  9232  prodge0i  9233  iccshftri  10380  iccshftli  10382  iccdili  10384  icccntri  10386  mulexpzap  10999  expaddzap  11003  m1expeven  11006  iexpcyc  11064  amgm2  11867  ege2le3  12421  sqnprm  12897  lmres  15332  2logb9irrap  16062