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  3417  ordtri2orexmid  4522  opthreg  4555  ordtri2or2exmid  4570  ontri2orexmidim  4571  fvtp1  5727  nq0m0r  7454  nq02m  7463  gt0srpr  7746  map2psrprg  7803  pitoregt0  7847  axcnre  7879  addgt0  8404  addgegt0  8405  addgtge0  8406  addge0  8407  addgt0i  8444  addge0i  8445  addgegt0i  8446  add20i  8448  mulge0i  8576  recextlem1  8607  recap0  8641  recdivap  8674  recgt1  8853  prodgt0i  8864  prodge0i  8865  iccshftri  9994  iccshftli  9996  iccdili  9998  icccntri  10000  mulexpzap  10559  expaddzap  10563  m1expeven  10566  iexpcyc  10624  amgm2  11126  ege2le3  11678  sqnprm  12135  lmres  13718  2logb9irrap  14365