MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6rbb Structured version   Visualization version   GIF version

Theorem syl6rbb 277
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6rbb.1 (𝜑 → (𝜓𝜒))
syl6rbb.2 (𝜒𝜃)
Assertion
Ref Expression
syl6rbb (𝜑 → (𝜃𝜓))

Proof of Theorem syl6rbb
StepHypRef Expression
1 syl6rbb.1 . . 3 (𝜑 → (𝜓𝜒))
2 syl6rbb.2 . . 3 (𝜒𝜃)
31, 2syl6bb 276 . 2 (𝜑 → (𝜓𝜃))
43bicomd 213 1 (𝜑 → (𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197
This theorem is referenced by:  syl6rbbr  279  bibif  360  pm5.61  749  oranabs  919  necon4bid  2868  resopab2  5483  xpco  5713  funconstss  6375  xpopth  7251  map1  8077  ac6sfi  8245  supgtoreq  8417  rankr1bg  8704  alephsdom  8947  brdom7disj  9391  fpwwe2lem13  9502  nn0sub  11381  elznn0  11430  nn01to3  11819  supxrbnd1  12189  supxrbnd2  12190  rexuz3  14132  smueqlem  15259  qnumdenbi  15499  dfiso3  16480  lssne0  18999  pjfval2  20101  0top  20835  1stccn  21314  dscopn  22425  bcthlem1  23167  ovolgelb  23294  iblpos  23604  itgposval  23607  itgsubstlem  23856  sincosq3sgn  24297  sincosq4sgn  24298  lgsquadlem3  25152  colinearalg  25835  wlklnwwlkln2lem  26836  2pthdlem1  26895  wwlks2onsym  26924  rusgrnumwwlkb0  26938  numclwwlk2lem1  27356  numclwwlk2lem1OLD  27363  nmoo0  27774  leop3  29112  leoptri  29123  f1od2  29627  tltnle  29790  dfrdg4  32183  curf  33517  poimirlem28  33567  itgaddnclem2  33599  lfl1dim  34726  glbconxN  34982  2dim  35074  elpadd0  35413  dalawlem13  35487  diclspsn  36800  dihglb2  36948  dochsordN  36980  lzunuz  37648  uneqsn  38638  ntrclskb  38684  ntrneiel2  38701  infxrbnd2  39898  2reu4a  41510  funressnfv  41529  iccpartiltu  41683
  Copyright terms: Public domain W3C validator