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  3466  ordtri2orexmid  4592  opthreg  4625  ordtri2or2exmid  4640  ontri2orexmidim  4641  fvtp1  5823  nq0m0r  7611  nq02m  7620  gt0srpr  7903  map2psrprg  7960  pitoregt0  8004  axcnre  8036  addgt0  8563  addgegt0  8564  addgtge0  8565  addge0  8566  addgt0i  8603  addge0i  8604  addgegt0i  8605  add20i  8607  mulge0i  8735  recextlem1  8766  recap0  8800  recdivap  8833  recgt1  9012  prodgt0i  9023  prodge0i  9024  iccshftri  10159  iccshftli  10161  iccdili  10163  icccntri  10165  mulexpzap  10768  expaddzap  10772  m1expeven  10775  iexpcyc  10833  amgm2  11595  ege2le3  12148  sqnprm  12624  lmres  14887  2logb9irrap  15616