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  3129  moeq3  3260  reusv1  4633  reusv2lem1  4634  fveqf1o  6186  fliftcnv  6190  fliftfun  6191  undom  7603  pwdom  7667  onomeneq  7705  pwfilem  7812  ordiso  7939  ordtypelem8  7948  wdompwdom  8002  unxpwdom  8013  harwdom  8014  infeq5i  8051  cantnfcl  8084  cantnfclOLD  8114  cardiun  8361  infxpenlem  8389  dfac8b  8410  acnnum  8431  inffien  8442  dfac12lem2  8522  cdadom3  8566  cdainflem  8569  cdainf  8570  infunabs  8585  infcda  8586  infdif  8587  infdif2  8588  infmap2  8596  fictb  8623  cofsmo  8647  fin23lem21  8717  hsmexlem1  8804  iundomg  8914  iunctb  8947  fpwwe2lem9  9014  canthnum  9025  winalim2  9072  rankcf  9153  tskuni  9159  npomex  9372  hashun2  12425  swrd2lsw  12864  2swrd2eqwrdeq  12865  limsupgord  13269  summolem2  13512  zsum  13514  isinv  15026  invsym2  15029  invfun  15030  oppcsect2  15041  oppcinv  15042  efgcpbllemb  16642  frgpuplem  16659  gsumval3OLD  16777  gsumval3  16780  bwthOLD  19777  1stcfb  19812  1stcrestlem  19819  2ndcdisj2  19824  txdis1cn  20002  tx1stc  20017  tgphaus  20481  qustgplem  20485  tsmsxp  20523  xmeter  20802  bndth  21324  ovolctb2  21769  ovoliunlem1  21779  i1fd  21954  dvgt0lem2  22270  taylf  22621  efcvx  22709  logccv  22909  loglesqrt  22997  usgraidx2v  24258  frgra3vlem1  24865  numclwlk1lem2f1  24959  stadd3i  27032  strlem6  27040  dmct  27402  cnvct  27403  mptct  27406  mptctf  27409  sibfof  28148  subfaclefac  28486  erdsze2lem1  28513  erdsze2lem2  28514  snmlff  28640  prodmolem2  29035  zprod  29037  orderseqlem  29300  frrlem5c  29361  heicant  30017  pell1qrgaplem  30777  dnwech  30962  stoweid  31730  dirkercncflem2  31771  fourierdlem36  31810  usgedgvadf1  32249  usgedgvadf1ALT  32252  bnj97  33631  bnj553  33663  bnj966  33709  bnj1442  33812  dvhopellsm  36546