Theorem mp3an23 1482

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  sbciegf  3780  predeq1  6305  wrecseq1  8317  ac6sfi  9257  unfilem1  9278  fiint  9299  ordtypelem2  9494  infxpenc2  10028  dju0en  10181  cfsmolem  10275  axdc4lem  10460  1nqenq  10974  mul02lem1  11413  muleqadd  11885  2halves  12489  halfcl  12497  rehalfcl  12498  half0  12499  halfpos2  12500  halfnneg2  12502  halfaddsub  12504  nneo  12708  zeo  12710  peano5uzi  12713  fztp  13637  uzrdgxfr  14033  bcn2  14385  bcpasc  14387  hashxplem  14500  hashfun  14504  swrds2  15013  repsw2  15025  repsw3  15026  imre  15197  reim  15198  crim  15204  addcj  15237  imval2  15240  cnpart  15329  01sqrexlem7  15337  absmax  15419  binomfallfaclem2  16130  bpoly2  16147  bpoly3  16148  fsumcube  16150  efgt0  16195  sinf  16216  efi4p  16229  resin4p  16230  recos4p  16231  sinneg  16238  efival  16244  cosadd  16257  sinmul  16264  sinbnd  16272  cosbnd  16273  ef01bndlem  16276  sin01bnd  16277  cos01bnd  16278  sin01gt0  16282  cos01gt0  16283  sin02gt0  16284  rpnnen2lem11  16316  rpnnen2lem12  16317  odd2np1lem  16434  odd2np1  16435  pythagtriplem12  16922  pythagtriplem14  16924  pythagtriplem15  16925  pythagtriplem16  16926  pythagtriplem17  16927  pockthi  17003  prmreclem5  17016  prmreclem6  17017  prmlem0  17201  prdsplusg  17547  prdsmulr  17548  prdsvsca  17549  isghm  19344  odinf  19691  ogrpaddlt  20266  ofldlt1  21042  lbsexg  21352  ofldchr  21790  psgnghm2  21795  mopnex  24746  tngnm  24878  tngngp2  24879  tngngpd  24880  tngngp  24881  addccncf  25146  sub1cncf  25148  sub2cncf  25149  iihalf1  25160  iihalf2  25162  pjthlem1  25666  ovolunlem1a  25725  ovolunlem1  25726  opnmbllem  25830  vitalilem4  25840  iblcnlem1  26017  itgcnlem  26019  dvmptre  26198  dvmptim  26199  dvlipcn  26223  mdegldg  26293  aaliou3lem3  26577  aaliou3lem8  26578  sincosq1lem  26732  sincosq2sgn  26734  sincosq3sgn  26735  sincosq4sgn  26736  sinq12gt0  26742  abssinper  26756  coskpi  26758  sineq0  26759  coseq1  26760  efeq1  26763  resinf1o  26771  efif1olem2  26778  efif1olem4  26780  logneg2  26850  cxpsqrtlem  26937  cxpsqrt  26938  logsqrt  26939  1cubr  27077  leibpilem2  27176  basellem3  27317  ppiub  27438  chtublem  27445  chtub  27446  bcmax  27512  bcp1ctr  27513  bposlem2  27519  bposlem6  27523  bposlem9  27526  logdivsum  27767  elno  27880  mulscl  28397  4ipval2  31175  ipidsq  31177  dipcl  31179  dipcj  31181  ipasslem11  31307  hvmul0  31491  pjhthlem1  31858  h1de2bi  32021  spanunsni  32046  adjeu  32356  nmopge0  32378  nmfnge0  32394  opsqrlem6  32612  mdsl1i  32788  mdsl2bi  32790  mdexchi  32802  superpos  32821  atabsi  32868  dmdbr5ati  32889  cdj3lem1  32901  fpwrelmapffslem  33190  dp2cl  33312  dpfrac1  33324  cshw1s2  33387  oddpwdc  34852  eulerpartgbij  34870  subfacp1lem2a  35746  subfacp1lem5  35750  subfacp1lem6  35751  subfaclim  35754  sinccvglem  36238  dfon2lem3  36349  dfon2lem7  36353  wsuceq1  36379  clsun  36934  vtoclefex  38075  finxpreclem5  38136  sin2h  38351  cos2h  38352  tan2h  38353  poimirlem22  38378  poimirlem31  38387  opnmbllem0  38392  mblfinlem3  38395  itg2addnclem3  38409  ftc1cnnclem  38427  ftc1anclem6  38434  ftc2nc  38438  dvasin  38440  fdc  38482  constcncf  38499  heiborlem7  38554  atlatmstc  40179  lcmineqlem10  42891  lcmineqlem12  42893  facp2  42996  3rdpwhole  43154  sn-00idlem1  43260  0prjspnlem  43456  sn-isghm  43506  diophren  43641  oaabsb  44122  dftrcl3  44547  dfrtrcl3  44560  cotrclrcl  44569  lhe4.4ex1a  45140  dirkerper  46911  sinnpoly  47746  zlmodzxznm  49414  sinh-conventional  50652