Theorem syl3c 66

Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 7-Jul-2011.)

Hypotheses

Ref	Expression
syl3c.1	|- ( ph -> ps )
syl3c.2	|- ( ph -> ch )
syl3c.3	|- ( ph -> th )
syl3c.4	|- ( ps -> ( ch -> ( th -> ta ) ) )

Assertion

Ref	Expression
syl3c	|- ( ph -> ta )

Proof of Theorem syl3c

Step	Hyp	Ref	Expression
1		syl3c.3	. 2 |- ( ph -> th )
2		syl3c.1	. . 3 |- ( ph -> ps )
3		syl3c.2	. . 3 |- ( ph -> ch )
4		syl3c.4	. . 3 |- ( ps -> ( ch -> ( th -> ta ) ) )
5	2, 3, 4	sylc 65	. 2 |- ( ph -> ( th -> ta ) )
6	1, 5	mpd 15	1 |- ( ph -> ta )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  tfrlem1  7472  fodomr  8111  dffi3  8337  cantnflt  8569  cantnflem1c  8584  cantnflem1  8586  isfin2-2  9141  fin23lem17  9160  fin23lem39  9172  axdc3lem2  9273  ttukeylem5  9335  pwfseqlem5  9485  seqf1olem2  12841  wrdind  13476  wrd2ind  13477  relexpindlem  13803  rtrclind  13805  rlimclim1  14276  caucvgrlem  14403  o1fsum  14545  lcmneg  15316  prmind2  15398  rami  15719  ramcl  15733  poslubmo  17146  posglbmo  17147  pslem  17206  telgsums  18390  pgpfaclem2  18481  islbs3  19155  mplsubglem  19434  mpllsslem  19435  prmirredlem  19841  psgndif  19948  gsummatr01lem4  20464  lmcvg  21066  lmff  21105  lmmo  21184  1stcfb  21248  1stcelcls  21264  restnlly  21285  lly1stc  21299  kgeni  21340  cnmpt12  21470  cnmpt22  21477  filss  21657  flimopn  21779  flimrest  21787  tgpt0  21922  tsmsi  21937  tsmsxp  21958  nmoleub2lem2  22916  nmoleub3  22919  cfil3i  23067  equivcfil  23097  equivcau  23098  ovolicc2lem3  23287  ovolicc2  23290  vitalilem2  23378  vitalilem3  23379  itg2seq  23509  limciun  23658  dvferm1lem  23747  dvferm2lem  23749  dvcnvrelem1  23780  dvfsumrlim  23794  dvfsum2  23797  ftc1a  23800  ftc1lem4  23802  fta1glem2  23926  plyeq0lem  23966  dgrcolem2  24030  dgrco  24031  plydivlem4  24051  fta1lem  24062  vieta1  24067  scvxcvx  24712  wilthlem2  24795  ftalem3  24801  perfectlem2  24955  2sqlem6  25148  2sqlem8  25151  dchrisumlema  25177  dchrisumlem2  25179  gropd  25923  grstructd  25924  pthdepisspth  26631  pjoi0  28576  atomli  29241  archirng  29742  archiabllem1a  29745  archiabllem2a  29748  archiabl  29752  crefi  29914  pcmplfin  29927  sigaclcu  30180  measvun  30272  signsply0  30628  bnj1128  31058  bnj1204  31080  bnj1417  31109  noprefixmo  31848  neibastop2lem  32355  poimirlem31  33440  ftc1cnnclem  33483  sdclem2  33538  heibor1lem  33608  cvrat4  34729  hdmapval2  37124  ismrcd1  37261  relexpxpmin  38009  ee222  38708  ee333  38713  ee1111  38722  sbcoreleleq  38745  ordelordALT  38747  trsbc  38750  ee110  38902  ee101  38904  ee011  38906  ee100  38908  ee010  38910  ee001  38912  eel1111  38947  eel11111  38950  fnchoice  39188  fiiuncl  39234  mullimc  39848  islptre  39851  mullimcf  39855  addlimc  39880  stoweidlem20  40237  stoweidlem59  40276  perfectALTVlem2  41631