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

Theorem syl56 36
Description: Combine syl5 34 and syl6 35. (Contributed by NM, 14-Nov-2013.)
Hypotheses
Ref Expression
syl56.1 (𝜑𝜓)
syl56.2 (𝜒 → (𝜓𝜃))
syl56.3 (𝜃𝜏)
Assertion
Ref Expression
syl56 (𝜒 → (𝜑𝜏))

Proof of Theorem syl56
StepHypRef Expression
1 syl56.1 . 2 (𝜑𝜓)
2 syl56.2 . . 3 (𝜒 → (𝜓𝜃))
3 syl56.3 . . 3 (𝜃𝜏)
42, 3syl6 35 . 2 (𝜒 → (𝜓𝜏))
51, 4syl5 34 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:  spfwOLD  1963  nfald  2162  cbv2h  2268  exdistrf  2332  euind  3375  reuind  3393  sbcimdv  3480  sbcimdvOLD  3481  cores  5597  tz7.7  5708  tz7.49  7485  omsmolem  7678  php  8088  hta  8704  carddom2  8747  infdif  8975  isf32lem3  9121  alephval2  9338  cfpwsdom  9350  nqerf  9696  zeo  11407  o1rlimmul  14283  catideu  16257  catpropd  16290  ufileu  21633  iscau2  22983  scvxcvx  24612  issgon  29964  cvmsss2  30961  onsucconni  32075  onsucsuccmpi  32081  bj-ssbft  32281  bj-ax12v3ALT  32315  bj-cbv2hv  32370  bj-sbsb  32464  wl-dveeq12  32940  lpolsatN  36254  lpolpolsatN  36255  frege70  37706  sspwtrALT  38529  snlindsntor  41545  0setrec  41737
  Copyright terms: Public domain W3C validator