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  3486  ordtri2orexmid  4616  opthreg  4649  ordtri2or2exmid  4664  ontri2orexmidim  4665  fvtp1  5857  nq0m0r  7659  nq02m  7668  gt0srpr  7951  map2psrprg  8008  pitoregt0  8052  axcnre  8084  addgt0  8611  addgegt0  8612  addgtge0  8613  addge0  8614  addgt0i  8651  addge0i  8652  addgegt0i  8653  add20i  8655  mulge0i  8783  recextlem1  8814  recap0  8848  recdivap  8881  recgt1  9060  prodgt0i  9071  prodge0i  9072  iccshftri  10208  iccshftli  10210  iccdili  10212  icccntri  10214  mulexpzap  10818  expaddzap  10822  m1expeven  10825  iexpcyc  10883  amgm2  11650  ege2le3  12203  sqnprm  12679  lmres  14943  2logb9irrap  15672