Theorem mp3an2 1362

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

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

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 1007

This theorem is referenced by:  mp3anl2  1369  ordin  4511  ordsuc  4690  omv  6701  oeiv  6702  omv2  6711  1idprl  7921  muladd11  8422  negsub  8537  subneg  8538  ltaddneg  8715  muleqadd  8959  diveqap1  8996  conjmulap  9020  nnsub  9293  addltmul  9492  zltp1le  9649  gtndiv  9691  eluzp1m1  9896  xnn0le2is012  10218  divelunit  10354  fznatpl1  10432  flqbi2  10675  flqdiv  10707  frecfzen2  10813  nn0ennn  10819  seqshft2g  10868  seqf1oglem1  10905  faclbnd3  11130  ccatrid  11320  shftfvalg  11528  ovshftex  11529  shftfval  11531  abs2dif  11816  cos2t  12461  sin01gt0  12473  cos01gt0  12474  demoivre  12484  demoivreALT  12485  omeo  12609  gcd0id  12700  sqgcd  12750  isprm3  12840  eulerthlemth  12954  pczpre  13020  pcrec  13031  setscom  13336  setsslid  13347  setsslnid  13348  mulgm1  13895  abssinper  15837  lgs1  16043