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

Theorem syl6rbbr 272
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
Hypotheses
Ref Expression
syl6rbbr.1  |-  ( ph  ->  ( ps  <->  ch )
)
syl6rbbr.2  |-  ( th  <->  ch )
Assertion
Ref Expression
syl6rbbr  |-  ( ph  ->  ( th  <->  ps )
)

Proof of Theorem syl6rbbr
StepHypRef Expression
1 syl6rbbr.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 syl6rbbr.2 . . 3  |-  ( th  <->  ch )
32bicomi 207 . 2  |-  ( ch  <->  th )
41, 3syl6rbb 270 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  baib  919  cad1  1527  necon2abid  2685  reu8  3222  sbc6g  3281  r19.28z  3852  r19.28zv  3855  r19.37zv  3856  r19.45zv  3857  r19.44zv  3858  r19.27z  3859  r19.27zv  3860  r19.36zv  3861  ralidm  3864  ralsnsg  3995  eldifvsn  4095  ssunsn2  4123  iunconst  4278  iinconst  4279  ordsseleq  5459  funssres  5629  fncnv  5657  fresaun  5766  dff1o5  5837  funimass4  5930  fndmdifeq0  6003  fneqeql2  6006  unpreima  6021  dffo3  6052  fnnfpeq0  6111  funfvima  6157  f1eqcocnv  6217  fliftf  6226  isocnv3  6241  isomin  6246  eloprabga  6402  mpt22eqb  6424  elpwun  6623  dfom2  6713  opabex3d  6790  opabex3  6791  f1oweALT  6796  fnwelem  6930  mptsuppd  6957  dfrecs3  7109  oe0m1  7241  oarec  7281  boxcutc  7583  ordunifi  7839  r1fin  8262  rankr1c  8310  iscard  8427  iscard2  8428  cardval2  8443  dfac3  8570  kmlem8  8605  infinf  9009  xrlenlt  9717  ltxrlt  9722  negcon2  9947  mulne0b  10275  dfinfre  10610  dfinfmrOLD  10611  crne0  10624  elznn  10977  zmax  11284  zq  11293  elfznelfzo  12045  hashneq0  12583  xpcogend  13113  sqrtneglem  13407  rexfiuz  13487  rexanuz2  13489  sumsplit  13906  fsum2dlem  13908  fsumcom2  13912  fprodcom2  14115  odd2np1  14443  divalgb  14464  gcdcllem2  14553  mrcidb2  15602  fncnvimaeqv  16083  lbsacsbs  18457  islpir2  18552  domnmuln0  18599  mplcoe1  18766  mplcoe5  18769  islinds2  19448  islbs4  19467  mamucl  19503  mavmulcl  19649  mdetunilem8  19721  iscld4  20158  iscon2  20506  kgencn  20648  tx1cn  20701  tx2cn  20702  elmptrab  20919  isfbas  20922  fbfinnfr  20934  cnfcf  21135  fmucndlem  21384  prdsxmslem2  21622  blval2  21655  cnbl0  21872  cnblcld  21873  metcld  22353  ismbf  22665  ismbfcn  22666  itg1val2  22721  itg2split  22786  itg2monolem1  22787  aannenlem1  23363  pilem1  23485  sinq34lt0t  23543  ellogrn  23588  logeftb  23612  ercgrg  24641  isusgra0  25153  usgraop  25156  constr3lem2  25453  ch0pss  27179  h1de2ctlem  27289  adjsym  27567  eigposi  27570  dfadj2  27619  elnlfn  27662  xppreima  28324  1stpreima  28362  2ndpreima  28363  qtophaus  28737  prsdm  28794  prsrn  28795  1stmbfm  29155  2ndmbfm  29156  eulerpartlemn  29287  bnj1454  29725  bnj984  29835  nofulllem1  30662  dffun10  30752  hfext  31021  isfne4b  31068  neifg  31098  taupilem3  31790  topdifinfindis  31819  topdifinffinlem  31820  finxpsuclem  31859  poimirlem23  32027  poimirlem26  32030  cnambfre  32053  0totbnd  32169  19.9alt  32602  cvrval2  32911  cvrnbtwn2  32912  cvrnbtwn4  32916  hlateq  33035  islpln5  33171  islvol5  33215  pmap11  33398  4atex  33712  cdleme0ex2N  33861  cdlemefrs29pre00  34033  diaord  34686  dihmeetlem13N  34958  lcfl1  35131  lcfls1N  35174  mapdpglem3  35314  isnacs2  35619  mrefg3  35621  pw2f1ocnv  35963  acsfn1p  36136  relexp0eq  36364  frege124d  36424  sbcoreleleq  36966  dffo3f  37521  climreeq  37790  funressnfv  38774  vtxd0nedgb  39711  vdiscusgrb  39753  wlkOnwlk1l  39861
  Copyright terms: Public domain W3C validator