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  3445  ordtri2orexmid  4559  opthreg  4592  ordtri2or2exmid  4607  ontri2orexmidim  4608  fvtp1  5773  nq0m0r  7523  nq02m  7532  gt0srpr  7815  map2psrprg  7872  pitoregt0  7916  axcnre  7948  addgt0  8475  addgegt0  8476  addgtge0  8477  addge0  8478  addgt0i  8515  addge0i  8516  addgegt0i  8517  add20i  8519  mulge0i  8647  recextlem1  8678  recap0  8712  recdivap  8745  recgt1  8924  prodgt0i  8935  prodge0i  8936  iccshftri  10070  iccshftli  10072  iccdili  10074  icccntri  10076  mulexpzap  10671  expaddzap  10675  m1expeven  10678  iexpcyc  10736  amgm2  11283  ege2le3  11836  sqnprm  12304  lmres  14484  2logb9irrap  15213