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  3432  ordtri2orexmid  4540  opthreg  4573  ordtri2or2exmid  4588  ontri2orexmidim  4589  fvtp1  5748  nq0m0r  7485  nq02m  7494  gt0srpr  7777  map2psrprg  7834  pitoregt0  7878  axcnre  7910  addgt0  8435  addgegt0  8436  addgtge0  8437  addge0  8438  addgt0i  8475  addge0i  8476  addgegt0i  8477  add20i  8479  mulge0i  8607  recextlem1  8638  recap0  8672  recdivap  8705  recgt1  8884  prodgt0i  8895  prodge0i  8896  iccshftri  10025  iccshftli  10027  iccdili  10029  icccntri  10031  mulexpzap  10591  expaddzap  10595  m1expeven  10598  iexpcyc  10656  amgm2  11159  ege2le3  11711  sqnprm  12168  lmres  14205  2logb9irrap  14852