Theorem mp3an2 1338

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 981

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

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  mp3anl2  1345  ordin  4433  ordsuc  4612  omv  6543  oeiv  6544  omv2  6553  1idprl  7705  muladd11  8207  negsub  8322  subneg  8323  ltaddneg  8499  muleqadd  8743  diveqap1  8780  conjmulap  8804  nnsub  9077  addltmul  9276  zltp1le  9429  gtndiv  9470  eluzp1m1  9674  xnn0le2is012  9990  divelunit  10126  fznatpl1  10200  flqbi2  10436  flqdiv  10468  frecfzen2  10574  nn0ennn  10580  seqshft2g  10629  seqf1oglem1  10666  faclbnd3  10890  ccatrid  11066  shftfvalg  11162  ovshftex  11163  shftfval  11165  abs2dif  11450  cos2t  12094  sin01gt0  12106  cos01gt0  12107  demoivre  12117  demoivreALT  12118  omeo  12242  gcd0id  12333  sqgcd  12383  isprm3  12473  eulerthlemth  12587  pczpre  12653  pcrec  12664  setscom  12905  setsslid  12916  setsslnid  12917  mulgm1  13511  abssinper  15351  lgs1  15554