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  3446  ordtri2orexmid  4560  opthreg  4593  ordtri2or2exmid  4608  ontri2orexmidim  4609  fvtp1  5776  nq0m0r  7542  nq02m  7551  gt0srpr  7834  map2psrprg  7891  pitoregt0  7935  axcnre  7967  addgt0  8494  addgegt0  8495  addgtge0  8496  addge0  8497  addgt0i  8534  addge0i  8535  addgegt0i  8536  add20i  8538  mulge0i  8666  recextlem1  8697  recap0  8731  recdivap  8764  recgt1  8943  prodgt0i  8954  prodge0i  8955  iccshftri  10089  iccshftli  10091  iccdili  10093  icccntri  10095  mulexpzap  10690  expaddzap  10694  m1expeven  10697  iexpcyc  10755  amgm2  11302  ege2le3  11855  sqnprm  12331  lmres  14592  2logb9irrap  15321