Theorem mp3an23 1455

Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses

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

Assertion

Ref	Expression
mp3an23	⊢ (𝜑 → 𝜃)

Proof of Theorem mp3an23

Step	Hyp	Ref	Expression
1		mp3an23.1	. 2 ⊢ 𝜓
2		mp3an23.2	. . 3 ⊢ 𝜒
3		mp3an23.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an3 1452	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan2 691	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  sbciegf  3789  predeq1  6264  wrecseq1  8271  ac6sfi  9207  unfilem1  9230  fiint  9253  ordtypelem2  9448  infxpenc2  9953  dju0en  10107  cfsmolem  10201  axdc4lem  10386  1nqenq  10893  mul02lem1  11328  muleqadd  11800  2halves  12378  halfcl  12386  rehalfcl  12387  half0  12388  halfpos2  12389  halfnneg2  12391  halfaddsub  12393  nneo  12596  zeo  12598  peano5uzi  12601  fztp  13519  uzrdgxfr  13910  bcn2  14262  bcpasc  14264  hashxplem  14376  hashfun  14380  swrds2  14883  repsw2  14893  repsw3  14894  imre  15051  reim  15052  crim  15058  addcj  15091  imval2  15094  cnpart  15183  01sqrexlem7  15191  absmax  15273  binomfallfaclem2  15983  bpoly2  16000  bpoly3  16001  fsumcube  16003  efgt0  16048  sinf  16069  efi4p  16082  resin4p  16083  recos4p  16084  sinneg  16091  efival  16097  cosadd  16110  sinmul  16117  sinbnd  16125  cosbnd  16126  ef01bndlem  16129  sin01bnd  16130  cos01bnd  16131  sin01gt0  16135  cos01gt0  16136  sin02gt0  16137  rpnnen2lem11  16169  rpnnen2lem12  16170  odd2np1lem  16287  odd2np1  16288  pythagtriplem12  16774  pythagtriplem14  16776  pythagtriplem15  16777  pythagtriplem16  16778  pythagtriplem17  16779  pockthi  16855  prmreclem5  16868  prmreclem6  16869  prmlem0  17053  prdsplusg  17398  prdsmulr  17399  prdsvsca  17400  isghm  19130  odinf  19478  ogrpaddlt  20053  ofldlt1  20796  lbsexg  21107  ofldchr  21519  psgnghm2  21524  mopnex  24441  tngnm  24573  tngngp2  24574  tngngpd  24575  tngngp  24576  addccncf  24844  sub1cncf  24846  sub2cncf  24847  iihalf1  24859  iihalf2  24862  pjthlem1  25371  ovolunlem1a  25431  ovolunlem1  25432  opnmbllem  25536  vitalilem4  25546  iblcnlem1  25723  itgcnlem  25725  dvmptre  25907  dvmptim  25908  dvlipcn  25933  mdegldg  26005  aaliou3lem3  26286  aaliou3lem8  26287  sincosq1lem  26440  sincosq2sgn  26442  sincosq3sgn  26443  sincosq4sgn  26444  sinq12gt0  26450  abssinper  26464  coskpi  26466  sineq0  26467  coseq1  26468  efeq1  26471  resinf1o  26479  efif1olem2  26486  efif1olem4  26488  logneg2  26558  cxpsqrtlem  26645  cxpsqrt  26646  logsqrt  26647  1cubr  26786  leibpilem2  26885  basellem3  27027  ppiub  27149  chtublem  27156  chtub  27157  bcmax  27223  bcp1ctr  27224  bposlem2  27230  bposlem6  27234  bposlem9  27237  logdivsum  27478  elno  27591  mulscl  28078  4ipval2  30688  ipidsq  30690  dipcl  30692  dipcj  30694  ipasslem11  30820  hvmul0  31004  pjhthlem1  31371  h1de2bi  31534  spanunsni  31559  adjeu  31869  nmopge0  31891  nmfnge0  31907  opsqrlem6  32125  mdsl1i  32301  mdsl2bi  32303  mdexchi  32315  superpos  32334  atabsi  32381  dmdbr5ati  32402  cdj3lem1  32414  fpwrelmapffslem  32706  dp2cl  32851  dpfrac1  32863  cshw1s2  32933  oddpwdc  34339  eulerpartgbij  34357  subfacp1lem2a  35161  subfacp1lem5  35165  subfacp1lem6  35166  subfaclim  35169  sinccvglem  35653  dfon2lem3  35767  dfon2lem7  35771  wsuceq1  35797  clsun  36310  vtoclefex  37316  finxpreclem5  37377  sin2h  37598  cos2h  37599  tan2h  37600  poimirlem22  37630  poimirlem31  37639  opnmbllem0  37644  mblfinlem3  37647  itg2addnclem3  37661  ftc1cnnclem  37679  ftc1anclem6  37686  ftc2nc  37690  dvasin  37692  fdc  37733  constcncf  37750  heiborlem7  37805  atlatmstc  39306  lcmineqlem10  42020  lcmineqlem12  42022  facp2  42125  3rdpwhole  42274  sn-00idlem1  42380  0prjspnlem  42605  sn-isghm  42655  diophren  42795  oaabsb  43277  dftrcl3  43703  dfrtrcl3  43716  cotrclrcl  43725  lhe4.4ex1a  44312  dirkerper  46088  sinnpoly  46886  zlmodzxznm  48480  sinh-conventional  49722