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  3489  ordtri2orexmid  4621  opthreg  4654  ordtri2or2exmid  4669  ontri2orexmidim  4670  fvtp1  5865  nq0m0r  7676  nq02m  7685  gt0srpr  7968  map2psrprg  8025  pitoregt0  8069  axcnre  8101  addgt0  8628  addgegt0  8629  addgtge0  8630  addge0  8631  addgt0i  8668  addge0i  8669  addgegt0i  8670  add20i  8672  mulge0i  8800  recextlem1  8831  recap0  8865  recdivap  8898  recgt1  9077  prodgt0i  9088  prodge0i  9089  iccshftri  10230  iccshftli  10232  iccdili  10234  icccntri  10236  mulexpzap  10842  expaddzap  10846  m1expeven  10849  iexpcyc  10907  amgm2  11680  ege2le3  12234  sqnprm  12710  lmres  14975  2logb9irrap  15704