Theorem mpanl12 412

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 410	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 400	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  reuun1  3219  ordtri2orexmid  4248  opthreg  4280  ordtri2or2exmid  4296  fvtp1  5372  nq0m0r  6552  nq02m  6561  gt0srpr  6831  pitoregt0  6923  axcnre  6953  addgt0  7441  addgegt0  7442  addgtge0  7443  addge0  7444  addgt0i  7478  addge0i  7479  addgegt0i  7480  add20i  7482  mulge0i  7609  recextlem1  7630  recap0  7662  recdivap  7692  recgt1  7861  prodgt0i  7872  prodge0i  7873  iccshftri  8861  iccshftli  8863  iccdili  8865  icccntri  8867  mulexpzap  9269  expaddzap  9273  amgm2  9688