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  3241  moeq3  3383  reusv1OLD  4867  fveqf1o  6557  fliftcnv  6561  fliftfun  6562  cnvct  8033  undom  8048  pwdom  8112  onomeneq  8150  pwfilem  8260  ordiso  8421  ordtypelem8  8430  wdompwdom  8483  unxpwdom  8494  harwdom  8495  infeq5i  8533  cantnfcl  8564  cardiun  8808  infxpenlem  8836  dfac8b  8854  acnnum  8875  inffien  8886  dfac12lem2  8966  cdadom3  9010  cdainflem  9013  cdainf  9014  infunabs  9029  infcda  9030  infdif  9031  infdif2  9032  infmap2  9040  fictb  9067  cofsmo  9091  fin23lem21  9161  hsmexlem1  9248  dmct  9346  mptct  9360  iundomg  9363  iunctb  9396  fpwwe2lem9  9460  canthnum  9471  winalim2  9518  rankcf  9599  tskuni  9605  npomex  9818  hashun2  13172  swrd2lsw  13695  2swrd2eqwrdeq  13696  limsupgord  14203  summolem2  14447  zsum  14449  prodmolem2  14665  zprod  14667  ltoddhalfle  15085  isinv  16420  invsym2  16423  invfun  16424  oppcsect2  16439  oppcinv  16440  efgcpbllemb  18168  frgpuplem  18185  gsumval3  18308  1stcfb  21248  1stcrestlem  21255  2ndcdisj2  21260  txdis1cn  21438  tx1stc  21453  tgphaus  21920  qustgplem  21924  tsmsxp  21958  xmeter  22238  bndth  22757  clmneg1  22882  ovolctb2  23260  ovoliunlem1  23270  i1fd  23448  dvgt0lem2  23766  taylf  24115  efcvx  24203  logccv  24409  loglesqrt  24499  usgredg2v  26119  crctcshtrl  26715  frgr3vlem1  27137  numclwlk1lem2f1  27227  strlem6  29115  mptctf  29495  omsmeas  30385  sibfof  30402  bnj97  30936  bnj553  30968  bnj966  31014  bnj1442  31117  subfaclefac  31158  erdsze2lem1  31185  erdsze2lem2  31186  snmlff  31311  orderseqlem  31749  frrlem5c  31786  bj-ssbid2ALT  32646  phpreu  33393  ptrecube  33409  poimirlem3  33412  poimirlem32  33441  heicant  33444  dvhopellsm  36406  pell1qrgaplem  37437  dnwech  37618  stoweid  40280  dirkercncflem2  40321  fourierdlem36  40360