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  3054  moeq3  3185  reusv1  4562  reusv2lem1  4563  fveqf1o  6154  fliftcnv  6158  fliftfun  6159  undom  7608  pwdom  7672  onomeneq  7710  pwfilem  7816  ordiso  7979  ordtypelem8  7988  wdompwdom  8041  unxpwdom  8052  harwdom  8053  infeq5i  8089  cantnfcl  8119  cardiun  8363  infxpenlem  8391  dfac8b  8408  acnnum  8429  inffien  8440  dfac12lem2  8520  cdadom3  8564  cdainflem  8567  cdainf  8568  infunabs  8583  infcda  8584  infdif  8585  infdif2  8586  infmap2  8594  fictb  8621  cofsmo  8645  fin23lem21  8715  hsmexlem1  8802  iundomg  8912  iunctb  8945  fpwwe2lem9  9009  canthnum  9020  winalim2  9067  rankcf  9148  tskuni  9154  npomex  9367  hashun2  12507  swrd2lsw  12966  2swrd2eqwrdeq  12967  limsupgord  13466  summolem2  13720  zsum  13722  prodmolem2  13927  zprod  13929  isinv  15603  invsym2  15606  invfun  15607  oppcsect2  15622  oppcinv  15623  efgcpbllemb  17343  frgpuplem  17360  gsumval3  17479  1stcfb  20397  1stcrestlem  20404  2ndcdisj2  20409  txdis1cn  20587  tx1stc  20602  tgphaus  21068  qustgplem  21072  tsmsxp  21106  xmeter  21385  bndth  21923  ovolctb2  22382  ovoliunlem1  22392  i1fd  22576  dvgt0lem2  22892  taylf  23253  efcvx  23341  logccv  23545  loglesqrt  23635  usgraidx2v  25057  frgra3vlem1  25665  numclwlk1lem2f1  25759  stadd3i  27838  strlem6  27846  dmct  28243  cnvct  28244  mptct  28247  mptctf  28250  omsmeas  29102  omsmeasOLD  29103  sibfof  29120  bnj97  29624  bnj553  29656  bnj966  29702  bnj1442  29805  subfaclefac  29846  erdsze2lem1  29873  erdsze2lem2  29874  snmlff  29999  orderseqlem  30436  frrlem5c  30466  phpreu  31836  ptrecube  31847  poimirlem3  31850  poimirlem32  31879  heicant  31882  dvhopellsm  34597  pell1qrgaplem  35632  dnwech  35819  stoweid  37808  dirkercncflem2  37849  fourierdlem36  37889  usgridx2v  39051  usgedgvadf1  39318  usgedgvadf1ALT  39321