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  905  nfimd  1886  sbi1vOLD  2314  nfald  2338  cbv2w  2348  cbv2  2414  cbv2h  2417  exdistrf  2461  mo4  2643  vtoclgft  3551  euind  3712  reuind  3741  sbcimdv  3840  cores  6095  tz7.7  6210  oprabidw  7176  tz7.49  8070  omsmolem  8269  php  8689  hta  9314  carddom2  9394  infdif  9619  isf32lem3  9765  alephval2  9982  cfpwsdom  9994  nqerf  10340  zeo  12056  o1rlimmul  14963  catideu  16934  catpropd  16967  ufileu  22455  iscau2  23807  scvxcvx  25490  issgon  31281  cvmsss2  32418  satffunlem2lem1  32548  onsucconni  33682  onsucsuccmpi  33688  bj-peircestab  33785  bj-cbvalimt  33869  bj-cbveximt  33870  bj-ax12v3ALT  33917  bj-wnf2  33949  bj-cbv2hv  34016  bj-sbsb  34057  bj-nfald  34321  lpolsatN  38504  lpolpolsatN  38505  frege70  40157  sspwtrALT  41033  snlindsntor  44454  0setrec  44734
  Copyright terms: Public domain W3C validator