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  3507  ordtri2orexmid  4650  opthreg  4683  ordtri2or2exmid  4698  ontri2orexmidim  4699  fvtp1  5900  nq0m0r  7787  nq02m  7796  gt0srpr  8079  map2psrprg  8136  pitoregt0  8180  axcnre  8212  addgt0  8740  addgegt0  8741  addgtge0  8742  addge0  8743  addgt0i  8780  addge0i  8781  addgegt0i  8782  add20i  8784  mulge0i  8912  recextlem1  8943  recap0  8979  recdivap  9012  recgt1  9191  prodgt0i  9202  prodge0i  9203  iccshftri  10350  iccshftli  10352  iccdili  10354  icccntri  10356  mulexpzap  10968  expaddzap  10972  m1expeven  10975  iexpcyc  11033  amgm2  11831  ege2le3  12385  sqnprm  12861  lmres  15242  2logb9irrap  15971