Theorem mp3an23 1456

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 1453	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan2 692	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  sbciegf  3778  predeq1  6260  wrecseq1  8257  ac6sfi  9186  unfilem1  9207  fiint  9229  ordtypelem2  9426  infxpenc2  9934  dju0en  10088  cfsmolem  10182  axdc4lem  10367  1nqenq  10875  mul02lem1  11311  muleqadd  11783  2halves  12361  halfcl  12369  rehalfcl  12370  half0  12371  halfpos2  12372  halfnneg2  12374  halfaddsub  12376  nneo  12578  zeo  12580  peano5uzi  12583  fztp  13498  uzrdgxfr  13892  bcn2  14244  bcpasc  14246  hashxplem  14358  hashfun  14362  swrds2  14865  repsw2  14875  repsw3  14876  imre  15033  reim  15034  crim  15040  addcj  15073  imval2  15076  cnpart  15165  01sqrexlem7  15173  absmax  15255  binomfallfaclem2  15965  bpoly2  15982  bpoly3  15983  fsumcube  15985  efgt0  16030  sinf  16051  efi4p  16064  resin4p  16065  recos4p  16066  sinneg  16073  efival  16079  cosadd  16092  sinmul  16099  sinbnd  16107  cosbnd  16108  ef01bndlem  16111  sin01bnd  16112  cos01bnd  16113  sin01gt0  16117  cos01gt0  16118  sin02gt0  16119  rpnnen2lem11  16151  rpnnen2lem12  16152  odd2np1lem  16269  odd2np1  16270  pythagtriplem12  16756  pythagtriplem14  16758  pythagtriplem15  16759  pythagtriplem16  16760  pythagtriplem17  16761  pockthi  16837  prmreclem5  16850  prmreclem6  16851  prmlem0  17035  prdsplusg  17380  prdsmulr  17381  prdsvsca  17382  isghm  19146  odinf  19494  ogrpaddlt  20069  ofldlt1  20810  lbsexg  21121  ofldchr  21533  psgnghm2  21538  mopnex  24465  tngnm  24597  tngngp2  24598  tngngpd  24599  tngngp  24600  addccncf  24868  sub1cncf  24870  sub2cncf  24871  iihalf1  24883  iihalf2  24886  pjthlem1  25395  ovolunlem1a  25455  ovolunlem1  25456  opnmbllem  25560  vitalilem4  25570  iblcnlem1  25747  itgcnlem  25749  dvmptre  25931  dvmptim  25932  dvlipcn  25957  mdegldg  26029  aaliou3lem3  26310  aaliou3lem8  26311  sincosq1lem  26464  sincosq2sgn  26466  sincosq3sgn  26467  sincosq4sgn  26468  sinq12gt0  26474  abssinper  26488  coskpi  26490  sineq0  26491  coseq1  26492  efeq1  26495  resinf1o  26503  efif1olem2  26510  efif1olem4  26512  logneg2  26582  cxpsqrtlem  26669  cxpsqrt  26670  logsqrt  26671  1cubr  26810  leibpilem2  26909  basellem3  27051  ppiub  27173  chtublem  27180  chtub  27181  bcmax  27247  bcp1ctr  27248  bposlem2  27254  bposlem6  27258  bposlem9  27261  logdivsum  27502  elno  27615  mulscl  28114  4ipval2  30764  ipidsq  30766  dipcl  30768  dipcj  30770  ipasslem11  30896  hvmul0  31080  pjhthlem1  31447  h1de2bi  31610  spanunsni  31635  adjeu  31945  nmopge0  31967  nmfnge0  31983  opsqrlem6  32201  mdsl1i  32377  mdsl2bi  32379  mdexchi  32391  superpos  32410  atabsi  32457  dmdbr5ati  32478  cdj3lem1  32490  fpwrelmapffslem  32790  dp2cl  32940  dpfrac1  32952  cshw1s2  33021  oddpwdc  34490  eulerpartgbij  34508  subfacp1lem2a  35353  subfacp1lem5  35357  subfacp1lem6  35358  subfaclim  35361  sinccvglem  35845  dfon2lem3  35956  dfon2lem7  35960  wsuceq1  35986  clsun  36501  vtoclefex  37508  finxpreclem5  37569  sin2h  37780  cos2h  37781  tan2h  37782  poimirlem22  37812  poimirlem31  37821  opnmbllem0  37826  mblfinlem3  37829  itg2addnclem3  37843  ftc1cnnclem  37861  ftc1anclem6  37868  ftc2nc  37872  dvasin  37874  fdc  37915  constcncf  37932  heiborlem7  37987  atlatmstc  39614  lcmineqlem10  42327  lcmineqlem12  42329  facp2  42432  3rdpwhole  42584  sn-00idlem1  42690  0prjspnlem  42903  sn-isghm  42953  diophren  43092  oaabsb  43573  dftrcl3  43998  dfrtrcl3  44011  cotrclrcl  44020  lhe4.4ex1a  44607  dirkerper  46377  sinnpoly  47174  zlmodzxznm  48780  sinh-conventional  50021