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  3418  ordtri2orexmid  4523  opthreg  4556  ordtri2or2exmid  4571  ontri2orexmidim  4572  fvtp1  5728  nq0m0r  7455  nq02m  7464  gt0srpr  7747  map2psrprg  7804  pitoregt0  7848  axcnre  7880  addgt0  8405  addgegt0  8406  addgtge0  8407  addge0  8408  addgt0i  8445  addge0i  8446  addgegt0i  8447  add20i  8449  mulge0i  8577  recextlem1  8608  recap0  8642  recdivap  8675  recgt1  8854  prodgt0i  8865  prodge0i  8866  iccshftri  9995  iccshftli  9997  iccdili  9999  icccntri  10001  mulexpzap  10560  expaddzap  10564  m1expeven  10567  iexpcyc  10625  amgm2  11127  ege2le3  11679  sqnprm  12136  lmres  13751  2logb9irrap  14398