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  3505  ordtri2orexmid  4647  opthreg  4680  ordtri2or2exmid  4695  ontri2orexmidim  4696  fvtp1  5897  nq0m0r  7776  nq02m  7785  gt0srpr  8068  map2psrprg  8125  pitoregt0  8169  axcnre  8201  addgt0  8727  addgegt0  8728  addgtge0  8729  addge0  8730  addgt0i  8767  addge0i  8768  addgegt0i  8769  add20i  8771  mulge0i  8899  recextlem1  8930  recap0  8964  recdivap  8997  recgt1  9176  prodgt0i  9187  prodge0i  9188  iccshftri  10334  iccshftli  10336  iccdili  10338  icccntri  10340  mulexpzap  10948  expaddzap  10952  m1expeven  10955  iexpcyc  11013  amgm2  11811  ege2le3  12365  sqnprm  12841  lmres  15162  2logb9irrap  15891