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  3488  ordtri2orexmid  4623  opthreg  4656  ordtri2or2exmid  4671  ontri2orexmidim  4672  fvtp1  5868  nq0m0r  7681  nq02m  7690  gt0srpr  7973  map2psrprg  8030  pitoregt0  8074  axcnre  8106  addgt0  8633  addgegt0  8634  addgtge0  8635  addge0  8636  addgt0i  8673  addge0i  8674  addgegt0i  8675  add20i  8677  mulge0i  8805  recextlem1  8836  recap0  8870  recdivap  8903  recgt1  9082  prodgt0i  9093  prodge0i  9094  iccshftri  10235  iccshftli  10237  iccdili  10239  icccntri  10241  mulexpzap  10847  expaddzap  10851  m1expeven  10854  iexpcyc  10912  amgm2  11701  ege2le3  12255  sqnprm  12731  lmres  15001  2logb9irrap  15730