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  3247  ordtri2orexmid  4268  opthreg  4301  ordtri2or2exmid  4316  fvtp1  5398  nq0m0r  6697  nq02m  6706  gt0srpr  6976  pitoregt0  7068  axcnre  7098  addgt0  7608  addgegt0  7609  addgtge0  7610  addge0  7611  addgt0i  7645  addge0i  7646  addgegt0i  7647  add20i  7649  mulge0i  7776  recextlem1  7797  recap0  7829  recdivap  7862  recgt1  8031  prodgt0i  8042  prodge0i  8043  iccshftri  9082  iccshftli  9084  iccdili  9086  icccntri  9088  mulexpzap  9602  expaddzap  9606  m1expeven  9609  iexpcyc  9665  amgm2  10131  sqnprm  10650