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  3456  ordtri2orexmid  4575  opthreg  4608  ordtri2or2exmid  4623  ontri2orexmidim  4624  fvtp1  5802  nq0m0r  7576  nq02m  7585  gt0srpr  7868  map2psrprg  7925  pitoregt0  7969  axcnre  8001  addgt0  8528  addgegt0  8529  addgtge0  8530  addge0  8531  addgt0i  8568  addge0i  8569  addgegt0i  8570  add20i  8572  mulge0i  8700  recextlem1  8731  recap0  8765  recdivap  8798  recgt1  8977  prodgt0i  8988  prodge0i  8989  iccshftri  10124  iccshftli  10126  iccdili  10128  icccntri  10130  mulexpzap  10731  expaddzap  10735  m1expeven  10738  iexpcyc  10796  amgm2  11473  ege2le3  12026  sqnprm  12502  lmres  14764  2logb9irrap  15493