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:  orim12dALT  936  nfimd  1993  sbi1v  2327  nfald  2351  nfeqf2OLD  2383  cbv2h  2408  exdistrf  2454  euind  3589  reuind  3609  sbcimdv  3695  cores  5857  tz7.7  5967  tz7.49  7779  omsmolem  7973  php  8386  hta  9010  carddom2  9089  infdif  9319  isf32lem3  9465  alephval2  9682  cfpwsdom  9694  nqerf  10040  zeo  11753  o1rlimmul  14690  catideu  16650  catpropd  16683  ufileu  22051  iscau2  23403  scvxcvx  25064  issgon  30702  cvmsss2  31773  onsucconni  32944  onsucsuccmpi  32950  bj-ssbft  33148  bj-ax12v3ALT  33182  bj-cbv2hv  33235  bj-sbsb  33319  lpolsatN  37509  lpolpolsatN  37510  frege70  39009  sspwtrALT  39818  snlindsntor  43059  0setrec  43249
  Copyright terms: Public domain W3C validator