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  3780  predeq1  6262  wrecseq1  8259  ac6sfi  9188  unfilem1  9209  fiint  9231  ordtypelem2  9428  infxpenc2  9936  dju0en  10090  cfsmolem  10184  axdc4lem  10369  1nqenq  10877  mul02lem1  11313  muleqadd  11785  2halves  12363  halfcl  12371  rehalfcl  12372  half0  12373  halfpos2  12374  halfnneg2  12376  halfaddsub  12378  nneo  12580  zeo  12582  peano5uzi  12585  fztp  13500  uzrdgxfr  13894  bcn2  14246  bcpasc  14248  hashxplem  14360  hashfun  14364  swrds2  14867  repsw2  14877  repsw3  14878  imre  15035  reim  15036  crim  15042  addcj  15075  imval2  15078  cnpart  15167  01sqrexlem7  15175  absmax  15257  binomfallfaclem2  15967  bpoly2  15984  bpoly3  15985  fsumcube  15987  efgt0  16032  sinf  16053  efi4p  16066  resin4p  16067  recos4p  16068  sinneg  16075  efival  16081  cosadd  16094  sinmul  16101  sinbnd  16109  cosbnd  16110  ef01bndlem  16113  sin01bnd  16114  cos01bnd  16115  sin01gt0  16119  cos01gt0  16120  sin02gt0  16121  rpnnen2lem11  16153  rpnnen2lem12  16154  odd2np1lem  16271  odd2np1  16272  pythagtriplem12  16758  pythagtriplem14  16760  pythagtriplem15  16761  pythagtriplem16  16762  pythagtriplem17  16763  pockthi  16839  prmreclem5  16852  prmreclem6  16853  prmlem0  17037  prdsplusg  17382  prdsmulr  17383  prdsvsca  17384  isghm  19148  odinf  19496  ogrpaddlt  20071  ofldlt1  20812  lbsexg  21123  ofldchr  21535  psgnghm2  21540  mopnex  24467  tngnm  24599  tngngp2  24600  tngngpd  24601  tngngp  24602  addccncf  24870  sub1cncf  24872  sub2cncf  24873  iihalf1  24885  iihalf2  24888  pjthlem1  25397  ovolunlem1a  25457  ovolunlem1  25458  opnmbllem  25562  vitalilem4  25572  iblcnlem1  25749  itgcnlem  25751  dvmptre  25933  dvmptim  25934  dvlipcn  25959  mdegldg  26031  aaliou3lem3  26312  aaliou3lem8  26313  sincosq1lem  26466  sincosq2sgn  26468  sincosq3sgn  26469  sincosq4sgn  26470  sinq12gt0  26476  abssinper  26490  coskpi  26492  sineq0  26493  coseq1  26494  efeq1  26497  resinf1o  26505  efif1olem2  26512  efif1olem4  26514  logneg2  26584  cxpsqrtlem  26671  cxpsqrt  26672  logsqrt  26673  1cubr  26812  leibpilem2  26911  basellem3  27053  ppiub  27175  chtublem  27182  chtub  27183  bcmax  27249  bcp1ctr  27250  bposlem2  27256  bposlem6  27260  bposlem9  27263  logdivsum  27504  elno  27617  mulscl  28134  4ipval2  30787  ipidsq  30789  dipcl  30791  dipcj  30793  ipasslem11  30919  hvmul0  31103  pjhthlem1  31470  h1de2bi  31633  spanunsni  31658  adjeu  31968  nmopge0  31990  nmfnge0  32006  opsqrlem6  32224  mdsl1i  32400  mdsl2bi  32402  mdexchi  32414  superpos  32433  atabsi  32480  dmdbr5ati  32501  cdj3lem1  32513  fpwrelmapffslem  32813  dp2cl  32963  dpfrac1  32975  cshw1s2  33044  oddpwdc  34513  eulerpartgbij  34531  subfacp1lem2a  35376  subfacp1lem5  35380  subfacp1lem6  35381  subfaclim  35384  sinccvglem  35868  dfon2lem3  35979  dfon2lem7  35983  wsuceq1  36009  clsun  36524  vtoclefex  37541  finxpreclem5  37602  sin2h  37813  cos2h  37814  tan2h  37815  poimirlem22  37845  poimirlem31  37854  opnmbllem0  37859  mblfinlem3  37862  itg2addnclem3  37876  ftc1cnnclem  37894  ftc1anclem6  37901  ftc2nc  37905  dvasin  37907  fdc  37948  constcncf  37965  heiborlem7  38020  atlatmstc  39647  lcmineqlem10  42360  lcmineqlem12  42362  facp2  42465  3rdpwhole  42614  sn-00idlem1  42720  0prjspnlem  42933  sn-isghm  42983  diophren  43122  oaabsb  43603  dftrcl3  44028  dfrtrcl3  44041  cotrclrcl  44050  lhe4.4ex1a  44637  dirkerper  46407  sinnpoly  47204  zlmodzxznm  48810  sinh-conventional  50051