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  3006  moeq3  3134  reusv1  4490  reusv2lem1  4491  fveqf1o  5998  fliftcnv  6002  fliftfun  6003  undom  7397  pwdom  7461  onomeneq  7498  pwfilem  7603  ordiso  7728  ordtypelem8  7737  wdompwdom  7791  unxpwdom  7802  harwdom  7803  infeq5i  7840  cantnfcl  7873  cantnfclOLD  7903  cardiun  8150  infxpenlem  8178  dfac8b  8199  acnnum  8220  inffien  8231  dfac12lem2  8311  cdadom3  8355  cdainflem  8358  cdainf  8359  infunabs  8374  infcda  8375  infdif  8376  infdif2  8377  infmap2  8385  fictb  8412  cofsmo  8436  fin23lem21  8506  hsmexlem1  8593  iundomg  8703  iunctb  8736  fpwwe2lem9  8803  canthnum  8814  winalim2  8861  rankcf  8942  tskuni  8948  npomex  9163  hashun2  12144  swrd2lsw  12550  2swrd2eqwrdeq  12551  limsupgord  12948  summolem2  13191  zsum  13193  isinv  14696  invsym2  14699  invfun  14700  oppcsect2  14711  oppcinv  14712  efgcpbllemb  16250  frgpuplem  16267  gsumval3OLD  16380  gsumval3  16383  bwthOLD  19012  1stcfb  19047  1stcrestlem  19054  2ndcdisj2  19059  txdis1cn  19206  tx1stc  19221  tgphaus  19685  divstgplem  19689  tsmsxp  19727  xmeter  20006  bndth  20528  ovolctb2  20973  ovoliunlem1  20983  i1fd  21157  dvgt0lem2  21473  taylf  21824  efcvx  21912  logccv  22106  loglesqr  22194  usgraidx2v  23309  stadd3i  25650  strlem6  25658  dmct  26012  cnvct  26013  mptct  26016  mptctf  26019  subfaclefac  27062  erdsze2lem1  27089  erdsze2lem2  27090  snmlff  27216  prodmolem2  27446  zprod  27448  orderseqlem  27711  frrlem5c  27772  heicant  28423  pell1qrgaplem  29211  dnwech  29398  stoweid  29855  frgra3vlem1  30589  numclwlk1lem2f1  30684  bnj97  31856  bnj553  31888  bnj966  31934  bnj1442  32037  dvhopellsm  34759