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  907  nfimd  1888  sbi1vOLD  2317  nfald  2341  cbv2w  2351  cbv2  2419  cbv2h  2422  exdistrf  2466  mo4  2648  vtoclgft  3559  euind  3719  reuind  3748  sbcimdv  3847  cores  6100  tz7.7  6215  oprabidw  7179  tz7.49  8072  omsmolem  8270  php  8690  hta  9315  carddom2  9395  infdif  9620  isf32lem3  9766  alephval2  9983  cfpwsdom  9995  nqerf  10341  zeo  12057  o1rlimmul  14965  catideu  16936  catpropd  16969  ufileu  22443  iscau2  23795  scvxcvx  25477  issgon  31268  cvmsss2  32405  satffunlem2lem1  32535  onsucconni  33669  onsucsuccmpi  33675  bj-peircestab  33772  bj-cbvalimt  33856  bj-cbveximt  33857  bj-ax12v3ALT  33904  bj-wnf2  33936  bj-cbv2hv  34003  bj-sbsb  34044  bj-nfald  34308  lpolsatN  38491  lpolpolsatN  38492  frege70  40144  sspwtrALT  41021  snlindsntor  44358  0setrec  44638
  Copyright terms: Public domain W3C validator