Theorem mpanl12 436

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 434	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 424	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  3417  ordtri2orexmid  4520  opthreg  4553  ordtri2or2exmid  4568  ontri2orexmidim  4569  fvtp1  5724  nq0m0r  7450  nq02m  7459  gt0srpr  7742  map2psrprg  7799  pitoregt0  7843  axcnre  7875  addgt0  8399  addgegt0  8400  addgtge0  8401  addge0  8402  addgt0i  8439  addge0i  8440  addgegt0i  8441  add20i  8443  mulge0i  8571  recextlem1  8602  recap0  8636  recdivap  8669  recgt1  8848  prodgt0i  8859  prodge0i  8860  iccshftri  9989  iccshftli  9991  iccdili  9993  icccntri  9995  mulexpzap  10553  expaddzap  10557  m1expeven  10560  iexpcyc  10617  amgm2  11118  ege2le3  11670  sqnprm  12126  lmres  13530  2logb9irrap  14177