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:  fodomr  9006  dffi3  9301  cantnflt  9542  cantnflem1  9559  axdc3lem2  10321  seqf1olem2  13877  wrd2ind  14543  relexpindlem  14882  rtrclind  14884  o1fsum  15633  lcmneg  16414  prmind2  16496  rami  16822  ramcl  16836  pslem  18396  telgsums  19700  islbs3  20540  psgndif  20930  mplsubglem  21328  mpllsslem  21329  gsummatr01lem4  21930  lmmo  22654  cnmpt12  22941  cnmpt22  22948  filss  23127  flimopn  23249  flimrest  23257  cfil3i  24556  equivcfil  24586  equivcau  24587  ovolicc2lem3  24806  limciun  25181  dvcnvrelem1  25304  dvfsumrlim  25318  dvfsum2  25321  dgrco  25559  scvxcvx  26258  ftalem3  26347  2sqlem6  26694  2sqlem8  26697  dchrisumlema  26759  dchrisumlem2  26761  gropd  27781  grstructd  27782  pthdepisspth  28482  pjoi0  30458  atomli  31123  archirng  31819  archiabllem1a  31822  archiabllem2a  31825  archiabl  31829  crefi  32202  pcmplfin  32215  sigaclcu  32490  measvun  32582  signsply0  32937  bnj1128  33376  bnj1204  33398  bnj1417  33427  addsproplem1  34272  negsproplem1  34309  neibastop2lem  34728  poimirlem31  36005  ftc1cnnclem  36045  sdclem2  36097  heibor1lem  36164  cvrat4  37802  hdmapval2  40191  ismrcd1  40887  relexpxpmin  41752  ee222  42549  ee333  42554  ee1111  42563  sbcoreleleq  42582  ordelordALT  42584  trsbc  42587  ee110  42724  ee101  42726  ee011  42728  ee100  42730  ee010  42732  ee001  42734  eel11111  42770  fnchoice  42999  fiiuncl  43038  mullimc  43612  islptre  43615  mullimcf  43619  addlimc  43644  stoweidlem20  44016  stoweidlem59  44055  perfectALTVlem2  45669
  Copyright terms: Public domain W3C validator