Theorem mp3an23 1462

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

Syntax hints:   → wi 4   ∧ w3a 1093

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  sbciegf  3763  predeq1  6258  wrecseq1  8259  ac6sfi  9188  unfilem1  9209  fiint  9231  ordtypelem2  9428  infxpenc2  9939  dju0en  10093  cfsmolem  10187  axdc4lem  10372  1nqenq  10880  mul02lem1  11317  muleqadd  11789  2halves  12390  halfcl  12398  rehalfcl  12399  half0  12400  halfpos2  12401  halfnneg2  12403  halfaddsub  12405  nneo  12608  zeo  12610  peano5uzi  12613  fztp  13529  uzrdgxfr  13924  bcn2  14276  bcpasc  14278  hashxplem  14390  hashfun  14394  swrds2  14897  repsw2  14907  repsw3  14908  imre  15065  reim  15066  crim  15072  addcj  15105  imval2  15108  cnpart  15197  01sqrexlem7  15205  absmax  15287  binomfallfaclem2  16000  bpoly2  16017  bpoly3  16018  fsumcube  16020  efgt0  16065  sinf  16086  efi4p  16099  resin4p  16100  recos4p  16101  sinneg  16108  efival  16114  cosadd  16127  sinmul  16134  sinbnd  16142  cosbnd  16143  ef01bndlem  16146  sin01bnd  16147  cos01bnd  16148  sin01gt0  16152  cos01gt0  16153  sin02gt0  16154  rpnnen2lem11  16186  rpnnen2lem12  16187  odd2np1lem  16304  odd2np1  16305  pythagtriplem12  16792  pythagtriplem14  16794  pythagtriplem15  16795  pythagtriplem16  16796  pythagtriplem17  16797  pockthi  16873  prmreclem5  16886  prmreclem6  16887  prmlem0  17071  prdsplusg  17416  prdsmulr  17417  prdsvsca  17418  isghm  19185  odinf  19533  ogrpaddlt  20108  ofldlt1  20851  lbsexg  21161  ofldchr  21555  psgnghm2  21560  mopnex  24506  tngnm  24638  tngngp2  24639  tngngpd  24640  tngngp  24641  addccncf  24906  sub1cncf  24908  sub2cncf  24909  iihalf1  24920  iihalf2  24922  pjthlem1  25426  ovolunlem1a  25485  ovolunlem1  25486  opnmbllem  25590  vitalilem4  25600  iblcnlem1  25777  itgcnlem  25779  dvmptre  25958  dvmptim  25959  dvlipcn  25983  mdegldg  26053  aaliou3lem3  26332  aaliou3lem8  26333  sincosq1lem  26483  sincosq2sgn  26485  sincosq3sgn  26486  sincosq4sgn  26487  sinq12gt0  26493  abssinper  26507  coskpi  26509  sineq0  26510  coseq1  26511  efeq1  26514  resinf1o  26522  efif1olem2  26529  efif1olem4  26531  logneg2  26601  cxpsqrtlem  26688  cxpsqrt  26689  logsqrt  26690  1cubr  26828  leibpilem2  26927  basellem3  27068  ppiub  27189  chtublem  27196  chtub  27197  bcmax  27263  bcp1ctr  27264  bposlem2  27270  bposlem6  27274  bposlem9  27277  logdivsum  27518  elno  27631  mulscl  28148  4ipval2  30801  ipidsq  30803  dipcl  30805  dipcj  30807  ipasslem11  30933  hvmul0  31117  pjhthlem1  31484  h1de2bi  31647  spanunsni  31672  adjeu  31982  nmopge0  32004  nmfnge0  32020  opsqrlem6  32238  mdsl1i  32414  mdsl2bi  32416  mdexchi  32428  superpos  32447  atabsi  32494  dmdbr5ati  32515  cdj3lem1  32527  fpwrelmapffslem  32828  dp2cl  32962  dpfrac1  32974  cshw1s2  33043  oddpwdc  34550  eulerpartgbij  34568  subfacp1lem2a  35423  subfacp1lem5  35427  subfacp1lem6  35428  subfaclim  35431  sinccvglem  35915  dfon2lem3  36026  dfon2lem7  36030  wsuceq1  36056  clsun  36571  vtoclefex  37711  finxpreclem5  37772  sin2h  37992  cos2h  37993  tan2h  37994  poimirlem22  38024  poimirlem31  38033  opnmbllem0  38038  mblfinlem3  38041  itg2addnclem3  38055  ftc1cnnclem  38073  ftc1anclem6  38080  ftc2nc  38084  dvasin  38086  fdc  38127  constcncf  38144  heiborlem7  38199  atlatmstc  39826  lcmineqlem10  42538  lcmineqlem12  42540  facp2  42643  3rdpwhole  42784  sn-00idlem1  42890  0prjspnlem  43088  sn-isghm  43138  diophren  43273  oaabsb  43754  dftrcl3  44179  dfrtrcl3  44192  cotrclrcl  44201  lhe4.4ex1a  44788  dirkerper  46553  sinnpoly  47368  zlmodzxznm  49002  sinh-conventional  50243