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  8667  dffi3  8894  cantnflt  9134  cantnflem1  9151  axdc3lem2  9872  seqf1olem2  13409  wrd2ind  14084  relexpindlem  14421  rtrclind  14423  o1fsum  15167  lcmneg  15946  prmind2  16028  rami  16350  ramcl  16364  pslem  17815  telgsums  19112  islbs3  19926  mplsubglem  20213  mpllsslem  20214  psgndif  20745  gsummatr01lem4  21266  lmmo  21987  cnmpt12  22274  cnmpt22  22281  filss  22460  flimopn  22582  flimrest  22590  cfil3i  23871  equivcfil  23901  equivcau  23902  ovolicc2lem3  24119  limciun  24491  dvcnvrelem1  24613  dvfsumrlim  24627  dvfsum2  24630  dgrco  24864  scvxcvx  25562  ftalem3  25651  2sqlem6  25998  2sqlem8  26001  dchrisumlema  26063  dchrisumlem2  26065  gropd  26815  grstructd  26816  pthdepisspth  27515  pjoi0  29493  atomli  30158  archirng  30817  archiabllem1a  30820  archiabllem2a  30823  archiabl  30827  crefi  31111  pcmplfin  31124  sigaclcu  31376  measvun  31468  signsply0  31821  bnj1128  32262  bnj1204  32284  bnj1417  32313  noprefixmo  33202  neibastop2lem  33708  poimirlem31  34922  ftc1cnnclem  34964  sdclem2  35016  heibor1lem  35086  cvrat4  36578  hdmapval2  38967  ismrcd1  39293  relexpxpmin  40060  ee222  40834  ee333  40839  ee1111  40848  sbcoreleleq  40867  ordelordALT  40869  trsbc  40872  ee110  41009  ee101  41011  ee011  41013  ee100  41015  ee010  41017  ee001  41019  eel11111  41055  fnchoice  41284  fiiuncl  41325  mullimc  41895  islptre  41898  mullimcf  41902  addlimc  41927  stoweidlem20  42304  stoweidlem59  42343  perfectALTVlem2  43886
  Copyright terms: Public domain W3C validator