Theorem syl3c 61

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

Hypotheses

Ref	Expression
syl3c.1
syl3c.2
syl3c.3
syl3c.4

Assertion

Ref	Expression
syl3c

Proof of Theorem syl3c

Step	Hyp	Ref	Expression
1		syl3c.3	. 2
2		syl3c.1	. . 3
3		syl3c.2	. . 3
4		syl3c.4	. . 3
5	2, 3, 4	sylc 60	. 2
6	1, 5	mpd 15	1

Syntax hints:  ->wi 4

This theorem is referenced by:  tfrlem1  7064  fodomr  7688  dffi3  7911  cantnflt  8112  cantnflem1c  8127  cantnflem1  8129  cantnfltOLD  8142  cantnflem1cOLD  8150  cantnflem1OLD  8152  isfin2-2  8720  fin23lem17  8739  fin23lem39  8751  axdc3lem2  8852  ttukeylem5  8914  pwfseqlem5  9062  seqf1olem2  12147  wrdind  12702  wrd2ind  12703  rlimclim1  13368  caucvgrlem  13495  o1fsum  13627  prmind2  14228  rami  14533  ramcl  14547  poslubmo  15776  posglbmo  15777  pslem  15836  telgsums  17022  pgpfaclem2  17133  islbs3  17801  mplsubglem  18093  mpllsslem  18094  mplsubglemOLD  18095  mpllsslemOLD  18096  prmirredlem  18523  prmirredlemOLD  18526  psgndif  18638  gsummatr01lem4  19160  lmcvg  19763  lmff  19802  lmmo  19881  1stcfb  19946  1stcelcls  19962  restnlly  19983  lly1stc  19997  kgeni  20038  cnmpt12  20168  cnmpt22  20175  filss  20354  flimopn  20476  flimrest  20484  tgpt0  20617  tsmsi  20632  tsmsxp  20657  nmoleub2lem2  21599  nmoleub3  21602  cfil3i  21708  equivcfil  21738  equivcau  21739  ovolicc2lem3  21930  ovolicc2  21933  vitalilem2  22018  vitalilem3  22019  itg2seq  22149  limciun  22298  dvferm1lem  22385  dvferm2lem  22387  dvcnvrelem1  22418  dvfsumrlim  22432  dvfsum2  22435  ftc1a  22438  ftc1lem4  22440  fta1glem2  22567  plyeq0lem  22607  dgrcolem2  22671  dgrco  22672  plydivlem4  22692  fta1lem  22703  vieta1  22708  scvxcvx  23315  wilthlem2  23343  ftalem3  23348  perfectlem2  23505  2sqlem6  23644  2sqlem8  23647  dchrisumlema  23673  dchrisumlem2  23675  pthdepisspth  24576  pjoi0  26635  atomli  27301  archirng  27732  archiabllem1a  27735  archiabllem2a  27738  archiabl  27742  crefi  27850  pcmplfin  27863  sigaclcu  28117  measvun  28180  signsply0  28508  relexpindlem  29062  relexpind  29063  rtrclind  29072  ftc1cnnclem  30088  neibastop2lem  30178  sdclem2  30235  heibor1lem  30305  ismrcd1  30630  lcmneg  31209  fnchoice  31404  mullimc  31622  islptre  31625  mullimcf  31629  addlimc  31654  stoweidlem20  31802  stoweidlem59  31841  ee222  33271  ee333  33276  ee1111  33286  sbcoreleleq  33306  ordelordALT  33308  trsbc  33311  ee110  33463  ee101  33465  ee011  33467  ee100  33469  ee010  33471  ee001  33473  eel1111  33517  eel11111  33520  bnj1128  34046  bnj1204  34068  bnj1417  34097  cvrat4  35167  hdmapval2  37562

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