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

Theorem syl6rbbr 279
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
Hypotheses
Ref Expression
syl6rbbr.1 (𝜑 → (𝜓𝜒))
syl6rbbr.2 (𝜃𝜒)
Assertion
Ref Expression
syl6rbbr (𝜑 → (𝜃𝜓))

Proof of Theorem syl6rbbr
StepHypRef Expression
1 syl6rbbr.1 . 2 (𝜑 → (𝜓𝜒))
2 syl6rbbr.2 . . 3 (𝜃𝜒)
32bicomi 214 . 2 (𝜒𝜃)
41, 3syl6rbb 277 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:  baib  964  cad1  1595  necon2abid  2865  reueubd  3194  reu8  3435  sbc6g  3494  r19.28z  4096  r19.37zv  4100  r19.45zv  4101  r19.44zv  4102  r19.27z  4103  r19.36zv  4105  ralidm  4108  ralsnsg  4248  eldifvsn  4359  ssunsn2  4391  iunconst  4561  iinconst  4562  relsng  5257  ordsseleq  5790  ordequn  5866  funssres  5968  fncnv  6000  fresaun  6113  dff1o5  6184  funimass4  6286  fndmdifeq0  6363  fneqeql2  6366  unpreima  6381  dffo3  6414  fnnfpeq0  6485  funfvima  6532  f1eqcocnv  6596  fliftf  6605  isocnv3  6622  isomin  6627  eloprabga  6789  mpt22eqb  6811  elpwun  7019  dfom2  7109  opabex3d  7187  opabex3  7188  f1oweALT  7194  fnwelem  7337  mptsuppd  7363  dfrecs3  7514  oe0m1  7646  oarec  7687  boxcutc  7993  ordunifi  8251  r1fin  8674  rankr1c  8722  iscard  8839  iscard2  8840  cardval2  8855  dfac3  8982  kmlem8  9017  infinf  9426  xrlenlt  10141  ltxrlt  10146  negcon2  10372  mulne0b  10706  dfinfre  11042  crne0  11051  elznn  11431  zmax  11823  zq  11832  elfznelfzo  12613  modmuladdnn0  12754  hashneq0  13193  xpcogend  13759  sqrtneglem  14051  rexfiuz  14131  rexanuz2  14133  sumsplit  14543  fsum2dlem  14545  fsumcom2OLD  14550  fprodcom2OLD  14759  odd2np1  15112  divalgb  15174  gcdcllem2  15269  mrcidb2  16325  fncnvimaeqv  16807  lbsacsbs  19204  islpir2  19299  domnmuln0  19346  mplcoe1  19513  mplcoe5  19516  islinds2  20200  islbs4  20219  mamucl  20255  mavmulcl  20401  mdetunilem8  20473  iscld4  20917  isconn2  21265  kgencn  21407  tx1cn  21460  tx2cn  21461  elmptrab  21678  isfbas  21680  fbfinnfr  21692  cnfcf  21893  fmucndlem  22142  prdsxmslem2  22381  blval2  22414  cnbl0  22624  cnblcld  22625  metcld  23150  ismbf  23442  ismbfcn  23443  itg1val2  23496  itg2split  23561  itg2monolem1  23562  aannenlem1  24128  pilem1  24250  sinq34lt0t  24306  ellogrn  24351  logeftb  24375  gausslemma2dlem1a  25135  ercgrg  25457  usgredgffibi  26261  vtxd0nedgb  26440  vdiscusgrb  26482  upgrspthswlk  26690  s3wwlks2on  26922  frgrncvvdeqlem2  27280  ch0pss  28432  h1de2ctlem  28542  adjsym  28820  eigposi  28823  dfadj2  28872  elnlfn  28915  xppreima  29577  1stpreima  29612  2ndpreima  29613  qtophaus  30031  prsdm  30088  prsrn  30089  1stmbfm  30450  2ndmbfm  30451  eulerpartlemn  30571  reprdifc  30833  circlemeth  30846  bnj1454  31038  bnj984  31148  elintfv  31788  dffun10  32146  hfext  32415  isfne4b  32461  neifg  32491  taupilem3  33295  topdifinfindis  33324  topdifinffinlem  33325  finxpsuclem  33364  poimirlem23  33562  poimirlem26  33565  cnambfre  33588  0totbnd  33702  opelvvdif  34164  opelresALTV  34172  inecmo  34260  brxrn  34276  brin2  34307  eleccossin  34373  19.9alt  34570  cvrval2  34879  cvrnbtwn2  34880  cvrnbtwn4  34884  hlateq  35003  islpln5  35139  islvol5  35183  pmap11  35366  4atex  35680  cdleme0ex2N  35829  cdlemefrs29pre00  36000  diaord  36653  dihmeetlem13N  36925  lcfl1  37098  lcfls1N  37141  mapdpglem3  37281  isnacs2  37586  mrefg3  37588  pw2f1ocnv  37921  acsfn1p  38086  relexp0eq  38310  frege124d  38370  uneqsn  38638  k0004lem1  38762  sbcoreleleq  39062  dffo3f  39678  climreeq  40163  funressnfv  41529  fmtnorec2lem  41779
  Copyright terms: Public domain W3C validator