Theorem mpisyl 18

Description: A syllogism combined with a modus ponens inference. (Contributed by Alan Sare, 25-Jul-2011.)

Hypotheses

Ref	Expression
mpisyl.1	|- ( ph -> ps )
mpisyl.2	|- ch
mpisyl.3	|- ( ps -> ( ch -> th ) )

Assertion

Ref	Expression
mpisyl	|- ( ph -> th )

Proof of Theorem mpisyl

Step	Hyp	Ref	Expression
1		mpisyl.1	. 2 |- ( ph -> ps )
2		mpisyl.2	. . 3 |- ch
3		mpisyl.3	. . 3 |- ( ps -> ( ch -> th ) )
4	2, 3	mpi 17	. 2 |- ( ps -> th )
5	1, 4	syl 16	1 |- ( ph -> th )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  ceqsex  3142  moeq3  3273  reusv1  4640  reusv2lem1  4641  fveqf1o  6184  fliftcnv  6188  fliftfun  6189  undom  7595  pwdom  7659  onomeneq  7697  pwfilem  7803  ordiso  7930  ordtypelem8  7939  wdompwdom  7993  unxpwdom  8004  harwdom  8005  infeq5i  8042  cantnfcl  8075  cantnfclOLD  8105  cardiun  8352  infxpenlem  8380  dfac8b  8401  acnnum  8422  inffien  8433  dfac12lem2  8513  cdadom3  8557  cdainflem  8560  cdainf  8561  infunabs  8576  infcda  8577  infdif  8578  infdif2  8579  infmap2  8587  fictb  8614  cofsmo  8638  fin23lem21  8708  hsmexlem1  8795  iundomg  8905  iunctb  8938  fpwwe2lem9  9005  canthnum  9016  winalim2  9063  rankcf  9144  tskuni  9150  npomex  9363  hashun2  12406  swrd2lsw  12840  2swrd2eqwrdeq  12841  limsupgord  13244  summolem2  13487  zsum  13489  isinv  15004  invsym2  15007  invfun  15008  oppcsect2  15019  oppcinv  15020  efgcpbllemb  16562  frgpuplem  16579  gsumval3OLD  16692  gsumval3  16695  bwthOLD  19670  1stcfb  19705  1stcrestlem  19712  2ndcdisj2  19717  txdis1cn  19864  tx1stc  19879  tgphaus  20343  divstgplem  20347  tsmsxp  20385  xmeter  20664  bndth  21186  ovolctb2  21631  ovoliunlem1  21641  i1fd  21816  dvgt0lem2  22132  taylf  22483  efcvx  22571  logccv  22765  loglesqr  22853  usgraidx2v  24055  frgra3vlem1  24662  numclwlk1lem2f1  24757  stadd3i  26829  strlem6  26837  dmct  27195  cnvct  27196  mptct  27199  mptctf  27202  subfaclefac  28246  erdsze2lem1  28273  erdsze2lem2  28274  snmlff  28400  prodmolem2  28630  zprod  28632  orderseqlem  28895  frrlem5c  28956  heicant  29613  pell1qrgaplem  30400  dnwech  30587  stoweid  31318  usgedgvadf1  31817  usgedgvadf1ALT  31820  bnj97  32878  bnj553  32910  bnj966  32956  bnj1442  33059  dvhopellsm  35789