MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl3c Structured version   Visualization version   GIF version

Theorem syl3c 63
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
StepHypRef Expression
1 syl3c.3 . 2 (𝜑𝜃)
2 syl3c.1 . . 3 (𝜑𝜓)
3 syl3c.2 . . 3 (𝜑𝜒)
4 syl3c.4 . . 3 (𝜓 → (𝜒 → (𝜃𝜏)))
52, 3, 4sylc 62 . 2 (𝜑 → (𝜃𝜏))
61, 5mpd 15 1 (𝜑𝜏)
Colors of variables: wff setvar class
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  7333  fodomr  7970  dffi3  8194  cantnflt  8426  cantnflem1c  8441  cantnflem1  8443  isfin2-2  8998  fin23lem17  9017  fin23lem39  9029  axdc3lem2  9130  ttukeylem5  9192  pwfseqlem5  9338  seqf1olem2  12655  wrdind  13271  wrd2ind  13272  relexpindlem  13594  rtrclind  13596  rlimclim1  14067  caucvgrlem  14194  o1fsum  14329  lcmneg  15097  prmind2  15179  rami  15500  ramcl  15514  poslubmo  16912  posglbmo  16913  pslem  16972  telgsums  18156  pgpfaclem2  18247  islbs3  18919  mplsubglem  19198  mpllsslem  19199  prmirredlem  19602  psgndif  19709  gsummatr01lem4  20222  lmcvg  20815  lmff  20854  lmmo  20933  1stcfb  20997  1stcelcls  21013  restnlly  21034  lly1stc  21048  kgeni  21089  cnmpt12  21219  cnmpt22  21226  filss  21406  flimopn  21528  flimrest  21536  tgpt0  21671  tsmsi  21686  tsmsxp  21707  nmoleub2lem2  22652  nmoleub3  22655  cfil3i  22790  equivcfil  22820  equivcau  22821  ovolicc2lem3  23008  ovolicc2  23011  vitalilem2  23098  vitalilem3  23099  itg2seq  23229  limciun  23378  dvferm1lem  23465  dvferm2lem  23467  dvcnvrelem1  23498  dvfsumrlim  23512  dvfsum2  23515  ftc1a  23518  ftc1lem4  23520  fta1glem2  23644  plyeq0lem  23684  dgrcolem2  23748  dgrco  23749  plydivlem4  23769  fta1lem  23780  vieta1  23785  scvxcvx  24426  wilthlem2  24509  ftalem3  24515  perfectlem2  24669  2sqlem6  24862  2sqlem8  24865  dchrisumlema  24891  dchrisumlem2  24893  pthdepisspth  25867  pjoi0  27763  atomli  28428  archirng  28876  archiabllem1a  28879  archiabllem2a  28882  archiabl  28886  crefi  29045  pcmplfin  29058  sigaclcu  29310  measvun  29402  signsply0  29757  bnj1128  30115  bnj1204  30137  bnj1417  30166  neibastop2lem  31328  poimirlem31  32410  ftc1cnnclem  32453  sdclem2  32508  heibor1lem  32578  cvrat4  33547  hdmapval2  35942  ismrcd1  36079  relexpxpmin  36828  ee222  37529  ee333  37534  ee1111  37543  sbcoreleleq  37566  ordelordALT  37568  trsbc  37571  ee110  37723  ee101  37725  ee011  37727  ee100  37729  ee010  37731  ee001  37733  eel1111  37768  eel11111  37771  fnchoice  38011  fiiuncl  38059  mullimc  38484  islptre  38487  mullimcf  38491  addlimc  38516  stoweidlem20  38714  stoweidlem59  38753  perfectALTVlem2  39967  gropd  40263  grstructd  40264  pthdepissPth  40940
  Copyright terms: Public domain W3C validator