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  3502  ordtri2orexmid  4644  opthreg  4677  ordtri2or2exmid  4692  ontri2orexmidim  4693  fvtp1  5894  nq0m0r  7767  nq02m  7776  gt0srpr  8059  map2psrprg  8116  pitoregt0  8160  axcnre  8192  addgt0  8718  addgegt0  8719  addgtge0  8720  addge0  8721  addgt0i  8758  addge0i  8759  addgegt0i  8760  add20i  8762  mulge0i  8890  recextlem1  8921  recap0  8955  recdivap  8988  recgt1  9167  prodgt0i  9178  prodge0i  9179  iccshftri  10324  iccshftli  10326  iccdili  10328  icccntri  10330  mulexpzap  10937  expaddzap  10941  m1expeven  10944  iexpcyc  11002  amgm2  11796  ege2le3  12350  sqnprm  12826  lmres  15100  2logb9irrap  15829