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  4637  reusv2lem1  4638  fveqf1o  6180  fliftcnv  6184  fliftfun  6185  undom  7598  pwdom  7662  onomeneq  7700  pwfilem  7806  ordiso  7933  ordtypelem8  7942  wdompwdom  7996  unxpwdom  8007  harwdom  8008  infeq5i  8044  cantnfcl  8077  cantnfclOLD  8107  cardiun  8354  infxpenlem  8382  dfac8b  8403  acnnum  8424  inffien  8435  dfac12lem2  8515  cdadom3  8559  cdainflem  8562  cdainf  8563  infunabs  8578  infcda  8579  infdif  8580  infdif2  8581  infmap2  8589  fictb  8616  cofsmo  8640  fin23lem21  8710  hsmexlem1  8797  iundomg  8907  iunctb  8940  fpwwe2lem9  9005  canthnum  9016  winalim2  9063  rankcf  9144  tskuni  9150  npomex  9363  hashun2  12434  swrd2lsw  12881  2swrd2eqwrdeq  12882  limsupgord  13377  summolem2  13620  zsum  13622  prodmolem2  13824  zprod  13826  isinv  15248  invsym2  15251  invfun  15252  oppcsect2  15267  oppcinv  15268  efgcpbllemb  16972  frgpuplem  16989  gsumval3OLD  17107  gsumval3  17110  1stcfb  20112  1stcrestlem  20119  2ndcdisj2  20124  txdis1cn  20302  tx1stc  20317  tgphaus  20781  qustgplem  20785  tsmsxp  20823  xmeter  21102  bndth  21624  ovolctb2  22069  ovoliunlem1  22079  i1fd  22254  dvgt0lem2  22570  taylf  22922  efcvx  23010  logccv  23212  loglesqrt  23300  usgraidx2v  24595  frgra3vlem1  25202  numclwlk1lem2f1  25296  stadd3i  27365  strlem6  27373  dmct  27767  cnvct  27768  mptct  27771  mptctf  27774  omsmeas  28531  sibfof  28546  subfaclefac  28884  erdsze2lem1  28911  erdsze2lem2  28912  snmlff  29038  orderseqlem  29572  frrlem5c  29633  heicant  30289  pell1qrgaplem  31048  dnwech  31233  stoweid  32084  dirkercncflem2  32125  fourierdlem36  32164  usgedgvadf1  32787  usgedgvadf1ALT  32790  bnj97  34325  bnj553  34357  bnj966  34403  bnj1442  34506  dvhopellsm  37241