Theorem mp3an1 1358

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

Hypotheses

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

Assertion

Ref	Expression
mp3an1	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem mp3an1

Step	Hyp	Ref	Expression
1		mp3an1.1	. 2 ⊢ 𝜑
2		mp3an1.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expb 1228	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	1, 3	mpan 424	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

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

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 1004

This theorem is referenced by:  mp3an12  1361  mp3an1i  1364  mp3anl1  1365  mp3an  1371  mp3an2i  1376  mp3an3an  1377  tfrlem9  6465  rdgexgg  6524  oaexg  6594  omexg  6597  oeiexg  6599  oav2  6609  nnaordex  6674  mulidnq  7576  1idpru  7778  addgt0sr  7962  muladd11  8279  cnegex  8324  negsubdi  8402  renegcl  8407  mulneg1  8541  ltaddpos  8599  addge01  8619  rimul  8732  recclap  8826  recidap  8833  recidap2  8834  recdivap2  8872  divdiv23apzi  8912  ltmul12a  9007  lemul12a  9009  mulgt1  9010  ltmulgt11  9011  gt0div  9017  ge0div  9018  ltdiv23i  9073  8th4div3  9330  gtndiv  9542  nn0ind  9561  fnn0ind  9563  xrre2  10017  ioorebasg  10171  fzen  10239  elfz0ubfz0  10321  expubnd  10818  le2sq2  10837  bernneq  10882  expnbnd  10885  faclbnd6  10966  bccl  10989  hashfacen  11058  wrdred1hash  11115  ccatlid  11141  swrd0g  11192  shftfval  11332  mulreap  11375  caucvgrelemrec  11490  binom1p  11996  efi4p  12228  sinadd  12247  cosadd  12248  cos2t  12261  cos2tsin  12262  absefib  12282  efieq1re  12283  demoivreALT  12285  odd2np1  12384  opoe  12406  omoe  12407  opeo  12408  omeo  12409  gcdadd  12506  gcdmultiple  12541  algcvgblem  12571  algcvga  12573  isprm3  12640  coprm  12666  1arith2  12891  rmodislmod  14315  cnfldneg  14537  cnfldmulg  14540  cnfldexp  14541  zringmulg  14562  zringsubgval  14569  bl2ioo  15224  ioo2blex  15226  mpomulcn  15240  sinperlem  15482  logge0  15554  lgsdir2  15712  1lgs  15722