Theorem mpisyl 21

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 20	. 2 |- ( ps -> th )
5	1, 4	syl 17	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  3094  moeq3  3226  reusv1  4616  reusv2lem1  4617  fveqf1o  6224  fliftcnv  6228  fliftfun  6229  undom  7685  pwdom  7749  onomeneq  7787  pwfilem  7893  ordiso  8056  ordtypelem8  8065  wdompwdom  8118  unxpwdom  8129  harwdom  8130  infeq5i  8166  cantnfcl  8197  cardiun  8441  infxpenlem  8469  dfac8b  8487  acnnum  8508  inffien  8519  dfac12lem2  8599  cdadom3  8643  cdainflem  8646  cdainf  8647  infunabs  8662  infcda  8663  infdif  8664  infdif2  8665  infmap2  8673  fictb  8700  cofsmo  8724  fin23lem21  8794  hsmexlem1  8881  iundomg  8991  iunctb  9024  fpwwe2lem9  9088  canthnum  9099  winalim2  9146  rankcf  9227  tskuni  9233  npomex  9446  hashun2  12593  swrd2lsw  13075  2swrd2eqwrdeq  13076  limsupgord  13576  summolem2  13830  zsum  13832  prodmolem2  14037  zprod  14039  isinv  15713  invsym2  15716  invfun  15717  oppcsect2  15732  oppcinv  15733  efgcpbllemb  17453  frgpuplem  17470  gsumval3  17589  1stcfb  20508  1stcrestlem  20515  2ndcdisj2  20520  txdis1cn  20698  tx1stc  20713  tgphaus  21179  qustgplem  21183  tsmsxp  21217  xmeter  21496  bndth  22034  ovolctb2  22493  ovoliunlem1  22503  i1fd  22687  dvgt0lem2  23003  taylf  23364  efcvx  23452  logccv  23656  loglesqrt  23746  usgraidx2v  25168  frgra3vlem1  25776  numclwlk1lem2f1  25870  stadd3i  27949  strlem6  27957  dmct  28346  cnvct  28347  mptct  28350  mptctf  28353  omsmeas  29203  omsmeasOLD  29204  sibfof  29221  bnj97  29725  bnj553  29757  bnj966  29803  bnj1442  29906  subfaclefac  29947  erdsze2lem1  29974  erdsze2lem2  29975  snmlff  30100  orderseqlem  30538  frrlem5c  30568  bj-ssbid2ALT  31303  phpreu  31973  ptrecube  31984  poimirlem3  31987  poimirlem32  32016  heicant  32019  dvhopellsm  34729  pell1qrgaplem  35763  dnwech  35950  stoweid  37962  dirkercncflem2  38003  fourierdlem36  38043  usgredg2v  39353  usgedgvadf1  39999  usgedgvadf1ALT  40002