Theorem mp3an2 1257

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an2.1	⊢ 𝜓
mp3an2.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an2	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mp3an2

Step	Hyp	Ref	Expression
1		mp3an2.1	. 2 ⊢ 𝜓
2		mp3an2.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expa 1139	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 426	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 920

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 depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  mp3anl2  1264  ordin  4176  ordsuc  4342  omv  6148  oeiv  6149  omv2  6158  1idprl  7052  muladd11  7518  negsub  7633  subneg  7634  ltaddneg  7805  muleqadd  8035  diveqap1  8070  conjmulap  8094  nnsub  8354  addltmul  8544  zltp1le  8700  gtndiv  8737  eluzp1m1  8937  divelunit  9314  fznatpl1  9383  flqbi2  9587  flqdiv  9617  frecfzen2  9723  nn0ennn  9729  iseqshft2  9767  faclbnd3  9986  shftfvalg  10080  ovshftex  10081  shftfval  10083  abs2dif  10366  omeo  10678  gcd0id  10750  sqgcd  10798  isprm3  10880