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  943  cad1  1553  necon2abid  2833  reueubd  3159  reu8  3396  sbc6g  3455  r19.28z  4054  r19.37zv  4058  r19.45zv  4059  r19.44zv  4060  r19.27z  4061  r19.36zv  4063  ralidm  4066  ralsnsg  4207  eldifvsn  4317  ssunsn2  4350  iunconst  4520  iinconst  4521  ordsseleq  5740  ordequn  5816  funssres  5918  fncnv  5950  fresaun  6062  dff1o5  6133  funimass4  6234  fndmdifeq0  6309  fneqeql2  6312  unpreima  6327  dffo3  6360  fnnfpeq0  6429  funfvima  6477  f1eqcocnv  6541  fliftf  6550  isocnv3  6567  isomin  6572  eloprabga  6732  mpt22eqb  6754  elpwun  6962  dfom2  7052  opabex3d  7130  opabex3  7131  f1oweALT  7137  fnwelem  7277  mptsuppd  7303  dfrecs3  7454  oe0m1  7586  oarec  7627  boxcutc  7936  ordunifi  8195  r1fin  8621  rankr1c  8669  iscard  8786  iscard2  8787  cardval2  8802  dfac3  8929  kmlem8  8964  infinf  9373  xrlenlt  10088  ltxrlt  10093  negcon2  10319  mulne0b  10653  dfinfre  10989  crne0  10998  elznn  11378  zmax  11770  zq  11779  elfznelfzo  12557  modmuladdnn0  12697  hashneq0  13138  xpcogend  13694  sqrtneglem  13988  rexfiuz  14068  rexanuz2  14070  sumsplit  14480  fsum2dlem  14482  fsumcom2OLD  14487  fprodcom2OLD  14696  odd2np1  15046  divalgb  15108  gcdcllem2  15203  mrcidb2  16259  fncnvimaeqv  16741  lbsacsbs  19137  islpir2  19232  domnmuln0  19279  mplcoe1  19446  mplcoe5  19449  islinds2  20133  islbs4  20152  mamucl  20188  mavmulcl  20334  mdetunilem8  20406  iscld4  20850  isconn2  21198  kgencn  21340  tx1cn  21393  tx2cn  21394  elmptrab  21611  isfbas  21614  fbfinnfr  21626  cnfcf  21827  fmucndlem  22076  prdsxmslem2  22315  blval2  22348  cnbl0  22558  cnblcld  22559  metcld  23085  ismbf  23378  ismbfcn  23379  itg1val2  23432  itg2split  23497  itg2monolem1  23498  aannenlem1  24064  pilem1  24186  sinq34lt0t  24242  ellogrn  24287  logeftb  24311  gausslemma2dlem1a  25071  ercgrg  25393  usgredgffibi  26197  vtxd0nedgb  26365  vdiscusgrb  26407  upgrspthswlk  26615  s3wwlks2on  26830  frgrncvvdeqlem2  27144  ch0pss  28274  h1de2ctlem  28384  adjsym  28662  eigposi  28665  dfadj2  28714  elnlfn  28757  xppreima  29422  1stpreima  29458  2ndpreima  29459  qtophaus  29877  prsdm  29934  prsrn  29935  1stmbfm  30296  2ndmbfm  30297  eulerpartlemn  30417  reprdifc  30679  circlemeth  30692  bnj1454  30886  bnj984  30996  elintfv  31638  dffun10  31996  hfext  32265  isfne4b  32311  neifg  32341  taupilem3  33136  topdifinfindis  33165  topdifinffinlem  33166  finxpsuclem  33205  poimirlem23  33403  poimirlem26  33406  cnambfre  33429  0totbnd  33543  19.9alt  34071  cvrval2  34380  cvrnbtwn2  34381  cvrnbtwn4  34385  hlateq  34504  islpln5  34640  islvol5  34684  pmap11  34867  4atex  35181  cdleme0ex2N  35330  cdlemefrs29pre00  35502  diaord  36155  dihmeetlem13N  36427  lcfl1  36600  lcfls1N  36643  mapdpglem3  36783  isnacs2  37088  mrefg3  37090  pw2f1ocnv  37423  acsfn1p  37588  relexp0eq  37812  frege124d  37872  uneqsn  38141  k0004lem1  38265  sbcoreleleq  38565  dffo3f  39180  climreeq  39645  funressnfv  40971  fmtnorec2lem  41219
  Copyright terms: Public domain W3C validator