Theorem mp3an23 1358

Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses

Ref	Expression
mp3an23.1	|- ps
mp3an23.2	|- ch
mp3an23.3	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mp3an23	|- ( ph -> th )

Proof of Theorem mp3an23

Step	Hyp	Ref	Expression
1		mp3an23.1	. 2 |- ps
2		mp3an23.2	. . 3 |- ch
3		mp3an23.3	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
4	2, 3	mp3an3 1355	. 2 |- ( ( ph /\ ps ) -> th )
5	1, 4	mpan2 678	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ w3a 986

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 189  df-an 373  df-3an 988

This theorem is referenced by:  sbciegf  3301  predeq1  5385  wrecseq1  7036  ac6sfi  7820  unfilem1  7840  ordtypelem2  8039  infxpenc2  8458  cda0en  8614  cfsmolem  8705  axdc4lem  8890  1nqenq  9392  mul02lem1  9814  muleqadd  10263  halfcl  10845  rehalfcl  10846  half0  10847  2halves  10848  halfpos2  10849  halfnneg2  10851  halfaddsub  10853  nneo  11026  zeo  11028  peano5uzi  11031  fztp  11859  uzrdgxfr  12187  bcn2  12511  bcpasc  12513  hashxplem  12612  hashfun  12616  swrds2  13032  repsw2  13037  repsw3  13038  imre  13183  reim  13184  crim  13190  addcj  13223  imval2  13226  cnpart  13315  sqrlem7  13324  absmax  13404  binomfallfaclem2  14105  bpoly2  14122  bpoly3  14123  fsumcube  14125  efgt0  14169  sinf  14190  efi4p  14203  resin4p  14204  recos4p  14205  sinneg  14212  efival  14218  cosadd  14231  sinmul  14238  sinbnd  14246  cosbnd  14247  ef01bndlem  14250  sin01bnd  14251  cos01bnd  14252  sin01gt0  14256  cos01gt0  14257  sin02gt0  14258  rpnnen2lem11  14289  rpnnen2  14290  odd2np1lem  14376  odd2np1  14377  pythagtriplem12  14788  pythagtriplem14  14790  pythagtriplem15  14791  pythagtriplem16  14792  pythagtriplem17  14793  pockthi  14863  prmreclem5  14876  prmreclem6  14877  prmlem0  15089  prdsplusg  15368  prdsmulr  15369  prdsvsca  15370  odinf  17226  lbsexg  18399  psgnghm2  19161  mopnex  21546  tngnm  21671  tngngp2  21672  tngngpd  21673  tngngp  21674  addccncf  21960  iihalf1  21971  iihalf2  21973  pjthlem1  22403  ovolunlem1a  22461  ovolunlem1  22462  opnmbllem  22571  vitalilem4  22581  iblcnlem1  22757  itgcnlem  22759  dvmptre  22935  dvmptim  22936  dvlipcn  22958  mdegldg  23027  aaliou3lem3  23312  aaliou3lem8  23313  sincosq1lem  23464  sincosq2sgn  23466  sincosq3sgn  23467  sincosq4sgn  23468  sinq12gt0  23474  abssinper  23485  coskpi  23487  sineq0  23488  coseq1  23489  efeq1  23490  resinf1o  23497  efif1olem2  23504  efif1olem4  23506  logneg2  23576  cxpsqrtlem  23659  cxpsqrt  23660  logsqrt  23661  1cubr  23780  leibpilem1  23878  leibpilem2  23879  basellem3  24021  ppiub  24144  chtublem  24151  chtub  24152  bcmax  24218  bcp1ctr  24219  bposlem2  24225  bposlem6  24229  bposlem9  24232  logdivsum  24383  4ipval2  26356  4ipval3  26360  ipidsq  26361  dipcl  26363  dipcj  26365  ipasslem11  26493  hvmul0  26689  pjhthlem1  27056  h1de2bi  27219  spanunsni  27244  adjeu  27554  nmopge0  27576  nmfnge0  27592  opsqrlem6  27810  mdsl1i  27986  mdsl2bi  27988  mdexchi  28000  superpos  28019  atabsi  28066  dmdbr5ati  28087  cdj3lem1  28099  fpwrelmapffslem  28329  ogrpaddlt  28493  ofldlt1  28588  ofldchr  28589  oddpwdc  29199  eulerpartgbij  29217  subfacp1lem2a  29915  subfacp1lem5  29919  subfacp1lem6  29920  subfaclim  29923  sinccvglem  30328  dfon2lem3  30443  dfon2lem7  30447  wsuceq1  30510  clsun  30996  vtoclefex  31748  finxpreclem5  31799  sin2h  31947  cos2h  31948  tan2h  31949  poimirlem22  31974  poimirlem26  31978  poimirlem31  31983  opnmbllem0  31988  mblfinlem3  31991  dvtanlemOLD  32003  itg2addnclem3  32007  ftc1cnnclem  32027  ftc1anclem6  32034  ftc2nc  32038  dvasin  32040  fdc  32086  constcncf  32103  sub1cncf  32105  sub2cncf  32106  heiborlem7  32161  atlatmstc  32897  diophren  35668  dftrcl3  36324  dfrtrcl3  36337  cotrclrcl  36346  lhe4.4ex1a  36689  dirkerper  37968  upgrtrls  39679  upgrspths1wlk  39706  zlmodzxznm  40394  sinh-conventional  40563  dp2cl  40593  dpfrac1  40596