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

Theorem syl3c 66
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 65 . 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  7457  fodomr  8096  dffi3  8322  cantnflt  8554  cantnflem1c  8569  cantnflem1  8571  isfin2-2  9126  fin23lem17  9145  fin23lem39  9157  axdc3lem2  9258  ttukeylem5  9320  pwfseqlem5  9470  seqf1olem2  12824  wrdind  13458  wrd2ind  13459  relexpindlem  13784  rtrclind  13786  rlimclim1  14257  caucvgrlem  14384  o1fsum  14526  lcmneg  15297  prmind2  15379  rami  15700  ramcl  15714  poslubmo  17127  posglbmo  17128  pslem  17187  telgsums  18371  pgpfaclem2  18462  islbs3  19136  mplsubglem  19415  mpllsslem  19416  prmirredlem  19822  psgndif  19929  gsummatr01lem4  20445  lmcvg  21047  lmff  21086  lmmo  21165  1stcfb  21229  1stcelcls  21245  restnlly  21266  lly1stc  21280  kgeni  21321  cnmpt12  21451  cnmpt22  21458  filss  21638  flimopn  21760  flimrest  21768  tgpt0  21903  tsmsi  21918  tsmsxp  21939  nmoleub2lem2  22897  nmoleub3  22900  cfil3i  23048  equivcfil  23078  equivcau  23079  ovolicc2lem3  23268  ovolicc2  23271  vitalilem2  23359  vitalilem3  23360  itg2seq  23490  limciun  23639  dvferm1lem  23728  dvferm2lem  23730  dvcnvrelem1  23761  dvfsumrlim  23775  dvfsum2  23778  ftc1a  23781  ftc1lem4  23783  fta1glem2  23907  plyeq0lem  23947  dgrcolem2  24011  dgrco  24012  plydivlem4  24032  fta1lem  24043  vieta1  24048  scvxcvx  24693  wilthlem2  24776  ftalem3  24782  perfectlem2  24936  2sqlem6  25129  2sqlem8  25132  dchrisumlema  25158  dchrisumlem2  25160  gropd  25904  grstructd  25905  pthdepisspth  26612  pjoi0  28546  atomli  29211  archirng  29716  archiabllem1a  29719  archiabllem2a  29722  archiabl  29726  crefi  29888  pcmplfin  29901  sigaclcu  30154  measvun  30246  signsply0  30602  bnj1128  31032  bnj1204  31054  bnj1417  31083  noprefixmo  31822  neibastop2lem  32330  poimirlem31  33411  ftc1cnnclem  33454  sdclem2  33509  heibor1lem  33579  cvrat4  34548  hdmapval2  36943  ismrcd1  37080  relexpxpmin  37828  ee222  38528  ee333  38533  ee1111  38542  sbcoreleleq  38565  ordelordALT  38567  trsbc  38570  ee110  38722  ee101  38724  ee011  38726  ee100  38728  ee010  38730  ee001  38732  eel1111  38767  eel11111  38770  fnchoice  39008  fiiuncl  39054  mullimc  39648  islptre  39651  mullimcf  39655  addlimc  39680  stoweidlem20  40000  stoweidlem59  40039  perfectALTVlem2  41396
  Copyright terms: Public domain W3C validator