Theorem mp3an2 1261

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 1143	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 426	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

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

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 926

This theorem is referenced by:  mp3anl2  1268  ordin  4203  ordsuc  4369  omv  6198  oeiv  6199  omv2  6208  1idprl  7128  muladd11  7594  negsub  7709  subneg  7710  ltaddneg  7881  muleqadd  8111  diveqap1  8146  conjmulap  8170  nnsub  8432  addltmul  8622  zltp1le  8774  gtndiv  8811  eluzp1m1  9011  divelunit  9388  fznatpl1  9457  flqbi2  9663  flqdiv  9693  frecfzen2  9799  nn0ennn  9805  iseqshft2  9863  faclbnd3  10116  shftfvalg  10217  ovshftex  10218  shftfval  10220  abs2dif  10504  omeo  10980  gcd0id  11052  sqgcd  11100  isprm3  11182