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  3768  predeq1  6265  wrecseq1  8262  ac6sfi  9191  unfilem1  9212  fiint  9234  ordtypelem2  9431  infxpenc2  9941  dju0en  10095  cfsmolem  10189  axdc4lem  10374  1nqenq  10882  mul02lem1  11319  muleqadd  11791  2halves  12392  halfcl  12400  rehalfcl  12401  half0  12402  halfpos2  12403  halfnneg2  12405  halfaddsub  12407  nneo  12610  zeo  12612  peano5uzi  12615  fztp  13531  uzrdgxfr  13926  bcn2  14278  bcpasc  14280  hashxplem  14392  hashfun  14396  swrds2  14899  repsw2  14909  repsw3  14910  imre  15067  reim  15068  crim  15074  addcj  15107  imval2  15110  cnpart  15199  01sqrexlem7  15207  absmax  15289  binomfallfaclem2  16002  bpoly2  16019  bpoly3  16020  fsumcube  16022  efgt0  16067  sinf  16088  efi4p  16101  resin4p  16102  recos4p  16103  sinneg  16110  efival  16116  cosadd  16129  sinmul  16136  sinbnd  16144  cosbnd  16145  ef01bndlem  16148  sin01bnd  16149  cos01bnd  16150  sin01gt0  16154  cos01gt0  16155  sin02gt0  16156  rpnnen2lem11  16188  rpnnen2lem12  16189  odd2np1lem  16306  odd2np1  16307  pythagtriplem12  16794  pythagtriplem14  16796  pythagtriplem15  16797  pythagtriplem16  16798  pythagtriplem17  16799  pockthi  16875  prmreclem5  16888  prmreclem6  16889  prmlem0  17073  prdsplusg  17418  prdsmulr  17419  prdsvsca  17420  isghm  19187  odinf  19535  ogrpaddlt  20110  ofldlt1  20849  lbsexg  21160  ofldchr  21572  psgnghm2  21577  mopnex  24500  tngnm  24632  tngngp2  24633  tngngpd  24634  tngngp  24635  addccncf  24900  sub1cncf  24902  sub2cncf  24903  iihalf1  24914  iihalf2  24916  pjthlem1  25420  ovolunlem1a  25479  ovolunlem1  25480  opnmbllem  25584  vitalilem4  25594  iblcnlem1  25771  itgcnlem  25773  dvmptre  25952  dvmptim  25953  dvlipcn  25977  mdegldg  26047  aaliou3lem3  26327  aaliou3lem8  26328  sincosq1lem  26480  sincosq2sgn  26482  sincosq3sgn  26483  sincosq4sgn  26484  sinq12gt0  26490  abssinper  26504  coskpi  26506  sineq0  26507  coseq1  26508  efeq1  26511  resinf1o  26519  efif1olem2  26526  efif1olem4  26528  logneg2  26598  cxpsqrtlem  26685  cxpsqrt  26686  logsqrt  26687  1cubr  26825  leibpilem2  26924  basellem3  27066  ppiub  27187  chtublem  27194  chtub  27195  bcmax  27261  bcp1ctr  27262  bposlem2  27268  bposlem6  27272  bposlem9  27275  logdivsum  27516  elno  27629  mulscl  28146  4ipval2  30800  ipidsq  30802  dipcl  30804  dipcj  30806  ipasslem11  30932  hvmul0  31116  pjhthlem1  31483  h1de2bi  31646  spanunsni  31671  adjeu  31981  nmopge0  32003  nmfnge0  32019  opsqrlem6  32237  mdsl1i  32413  mdsl2bi  32415  mdexchi  32427  superpos  32446  atabsi  32493  dmdbr5ati  32514  cdj3lem1  32526  fpwrelmapffslem  32826  dp2cl  32960  dpfrac1  32972  cshw1s2  33041  oddpwdc  34520  eulerpartgbij  34538  subfacp1lem2a  35384  subfacp1lem5  35388  subfacp1lem6  35389  subfaclim  35392  sinccvglem  35876  dfon2lem3  35987  dfon2lem7  35991  wsuceq1  36017  clsun  36532  vtoclefex  37672  finxpreclem5  37733  sin2h  37953  cos2h  37954  tan2h  37955  poimirlem22  37985  poimirlem31  37994  opnmbllem0  37999  mblfinlem3  38002  itg2addnclem3  38016  ftc1cnnclem  38034  ftc1anclem6  38041  ftc2nc  38045  dvasin  38047  fdc  38088  constcncf  38105  heiborlem7  38160  atlatmstc  39787  lcmineqlem10  42499  lcmineqlem12  42501  facp2  42604  3rdpwhole  42746  sn-00idlem1  42852  0prjspnlem  43078  sn-isghm  43128  diophren  43267  oaabsb  43748  dftrcl3  44173  dfrtrcl3  44186  cotrclrcl  44195  lhe4.4ex1a  44782  dirkerper  46550  sinnpoly  47359  zlmodzxznm  48993  sinh-conventional  50234