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  4615  opthreg  4648  ordtri2or2exmid  4663  ontri2orexmidim  4664  fvtp1  5854  nq0m0r  7651  nq02m  7660  gt0srpr  7943  map2psrprg  8000  pitoregt0  8044  axcnre  8076  addgt0  8603  addgegt0  8604  addgtge0  8605  addge0  8606  addgt0i  8643  addge0i  8644  addgegt0i  8645  add20i  8647  mulge0i  8775  recextlem1  8806  recap0  8840  recdivap  8873  recgt1  9052  prodgt0i  9063  prodge0i  9064  iccshftri  10199  iccshftli  10201  iccdili  10203  icccntri  10205  mulexpzap  10809  expaddzap  10813  m1expeven  10816  iexpcyc  10874  amgm2  11637  ege2le3  12190  sqnprm  12666  lmres  14930  2logb9irrap  15659