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  3487  ordtri2orexmid  4619  opthreg  4652  ordtri2or2exmid  4667  ontri2orexmidim  4668  fvtp1  5860  nq0m0r  7669  nq02m  7678  gt0srpr  7961  map2psrprg  8018  pitoregt0  8062  axcnre  8094  addgt0  8621  addgegt0  8622  addgtge0  8623  addge0  8624  addgt0i  8661  addge0i  8662  addgegt0i  8663  add20i  8665  mulge0i  8793  recextlem1  8824  recap0  8858  recdivap  8891  recgt1  9070  prodgt0i  9081  prodge0i  9082  iccshftri  10223  iccshftli  10225  iccdili  10227  icccntri  10229  mulexpzap  10834  expaddzap  10838  m1expeven  10841  iexpcyc  10899  amgm2  11672  ege2le3  12225  sqnprm  12701  lmres  14965  2logb9irrap  15694