Theorem mpanl12 427

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

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  reuun1  3270  ordtri2orexmid  4311  opthreg  4344  ordtri2or2exmid  4359  fvtp1  5463  nq0m0r  6952  nq02m  6961  gt0srpr  7231  pitoregt0  7323  axcnre  7353  addgt0  7863  addgegt0  7864  addgtge0  7865  addge0  7866  addgt0i  7900  addge0i  7901  addgegt0i  7902  add20i  7904  mulge0i  8031  recextlem1  8052  recap0  8084  recdivap  8117  recgt1  8286  prodgt0i  8297  prodge0i  8298  iccshftri  9337  iccshftli  9339  iccdili  9341  icccntri  9343  mulexpzap  9886  expaddzap  9890  m1expeven  9893  iexpcyc  9949  amgm2  10439  sqnprm  10984