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  912  nfimd  1894  nfald  2328  cbv2w  2339  cbv2  2408  cbv2h  2411  exdistrf  2452  mo4  2566  euind  3730  reuind  3759  sbcimdv  3859  cores  6269  tz7.7  6410  oprabidw  7462  tz7.49  8485  omsmolem  8695  phpOLD  9259  hta  9937  carddom2  10017  infdif  10248  isf32lem3  10395  alephval2  10612  cfpwsdom  10624  nqerf  10970  zeo  12704  o1rlimmul  15655  catideu  17718  catpropd  17752  ufileu  23927  iscau2  25311  scvxcvx  27029  issgon  34124  cbvex1v  35088  cvmsss2  35279  satffunlem2lem1  35409  onsucconni  36438  onsucsuccmpi  36444  bj-peircestab  36554  bj-cbvalimt  36640  bj-cbveximt  36641  bj-ax12v3ALT  36687  bj-wnf2  36719  bj-cbv2hv  36798  bj-sbsb  36838  bj-nfald  37138  lpolsatN  41490  lpolpolsatN  41491  naddcnffo  43377  frege70  43946  sspwtrALT  44842  snlindsntor  48388  0setrec  49223
  Copyright terms: Public domain W3C validator