Theorem mpanl12 440

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 438	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 428	1 ⊢ (𝜒 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  reuun1  3515  ordtri2orexmid  4670  opthreg  4703  ordtri2or2exmid  4718  ontri2orexmidim  4719  fvtp1  5926  nq0m0r  7823  nq02m  7832  gt0srpr  8115  map2psrprg  8172  pitoregt0  8216  axcnre  8248  addgt0  8776  addgegt0  8777  addgtge0  8778  addge0  8779  addgt0i  8816  addge0i  8817  addgegt0i  8818  add20i  8820  mulge0i  8949  recextlem1  8980  recap0  9016  recdivap  9049  recgt1  9228  prodgt0i  9239  prodge0i  9240  iccshftri  10399  iccshftli  10401  iccdili  10403  icccntri  10405  mulexpzap  11018  expaddzap  11022  m1expeven  11025  iexpcyc  11083  amgm2  11886  ege2le3  12440  sqnprm  12916  lmres  15351  2logb9irrap  16085