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  911  nfimd  1898  nfald  2322  cbv2w  2334  cbv2  2402  cbv2h  2405  exdistrf  2446  mo4  2561  euind  3686  reuind  3715  sbcimdv  3817  sbcimdvOLD  3818  cores  6205  tz7.7  6347  oprabidw  7392  tz7.49  8395  omsmolem  8607  phpOLD  9172  hta  9841  carddom2  9921  infdif  10153  isf32lem3  10299  alephval2  10516  cfpwsdom  10528  nqerf  10874  zeo  12597  o1rlimmul  15510  catideu  17563  catpropd  17597  ufileu  23293  iscau2  24664  scvxcvx  26358  issgon  32786  cvmsss2  33932  satffunlem2lem1  34062  onsucconni  34962  onsucsuccmpi  34968  bj-peircestab  35069  bj-cbvalimt  35156  bj-cbveximt  35157  bj-ax12v3ALT  35204  bj-wnf2  35236  bj-cbv2hv  35315  bj-sbsb  35355  bj-nfald  35658  lpolsatN  40001  lpolpolsatN  40002  naddcnffo  41727  frege70  42297  sspwtrALT  43196  snlindsntor  46642  0setrec  47239
  Copyright terms: Public domain W3C validator