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  4652  opthreg  4685  ordtri2or2exmid  4700  ontri2orexmidim  4701  fvtp1  5902  nq0m0r  7789  nq02m  7798  gt0srpr  8081  map2psrprg  8138  pitoregt0  8182  axcnre  8214  addgt0  8742  addgegt0  8743  addgtge0  8744  addge0  8745  addgt0i  8782  addge0i  8783  addgegt0i  8784  add20i  8786  mulge0i  8914  recextlem1  8945  recap0  8981  recdivap  9014  recgt1  9193  prodgt0i  9204  prodge0i  9205  iccshftri  10352  iccshftli  10354  iccdili  10356  icccntri  10358  mulexpzap  10970  expaddzap  10974  m1expeven  10977  iexpcyc  11035  amgm2  11834  ege2le3  12388  sqnprm  12864  lmres  15245  2logb9irrap  15974