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  525  cad1  1703  necon2abid  2985  reueubd  3313  reu8  3554  sbc6g  3613  r19.28z  4204  r19.37zv  4208  r19.45zv  4209  r19.44zv  4210  r19.27z  4211  r19.36zv  4213  ralidm  4216  ralsnsg  4354  eldifvsn  4463  ssunsn2  4493  iunconst  4663  iinconst  4664  relsng  5363  ordsseleq  5895  ordequn  5971  funssres  6073  fncnv  6102  fresaun  6215  dff1o5  6287  funimass4  6389  fndmdifeq0  6466  fneqeql2  6469  unpreima  6484  dffo3  6517  fnnfpeq0  6588  funfvima  6635  f1eqcocnv  6699  fliftf  6708  isocnv3  6725  isomin  6730  eloprabga  6894  mpt22eqb  6916  elpwun  7124  dfom2  7214  opabex3d  7292  opabex3  7293  f1oweALT  7299  fnwelem  7443  mptsuppd  7469  dfrecs3  7622  oe0m1  7755  oarec  7796  boxcutc  8105  ordunifi  8366  r1fin  8800  rankr1c  8848  iscard  9001  iscard2  9002  cardval2  9017  dfac3  9144  kmlem8  9181  infinf  9590  xrlenlt  10305  ltxrlt  10310  negcon2  10536  mulne0b  10870  dfinfre  11206  crne0  11215  elznn  11595  zmax  11988  zq  11997  elfznelfzo  12781  modmuladdnn0  12922  hashneq0  13357  xpcogend  13923  sqrtneglem  14215  rexfiuz  14295  rexanuz2  14297  sumsplit  14707  fsum2dlem  14709  odd2np1  15273  divalgb  15335  gcdcllem2  15430  mrcidb2  16486  fncnvimaeqv  16967  lbsacsbs  19371  islpir2  19466  domnmuln0  19513  mplcoe1  19680  mplcoe5  19683  islinds2  20369  islbs4  20388  mamucl  20424  mavmulcl  20571  mdetunilem8  20643  iscld4  21090  isconn2  21438  kgencn  21580  tx1cn  21633  tx2cn  21634  elmptrab  21851  isfbas  21853  fbfinnfr  21865  cnfcf  22066  fmucndlem  22315  prdsxmslem2  22554  blval2  22587  cnbl0  22797  cnblcld  22798  metcld  23323  ismbf  23616  ismbfcn  23617  itg1val2  23671  itg2split  23736  itg2monolem1  23737  aannenlem1  24303  pilem1  24425  sinq34lt0t  24482  ellogrn  24527  logeftb  24551  gausslemma2dlem1a  25311  ercgrg  25633  usgredgffibi  26439  vtxd0nedgb  26619  vdiscusgrb  26661  upgrspthswlk  26869  s3wwlks2on  27104  frgrncvvdeqlem2  27482  ch0pss  28644  h1de2ctlem  28754  adjsym  29032  eigposi  29035  dfadj2  29084  elnlfn  29127  xppreima  29789  1stpreima  29824  2ndpreima  29825  qtophaus  30243  prsdm  30300  prsrn  30301  1stmbfm  30662  2ndmbfm  30663  eulerpartlemn  30783  reprdifc  31045  circlemeth  31058  bnj1454  31250  bnj984  31360  elintfv  32000  dffun10  32358  hfext  32627  isfne4b  32673  neifg  32703  taupilem3  33502  topdifinfindis  33531  topdifinffinlem  33532  finxpsuclem  33571  poimirlem23  33765  poimirlem26  33768  cnambfre  33790  0totbnd  33904  opelvvdif  34366  opelresALTV  34374  inecmo  34462  brxrn  34478  brin2  34509  eleccossin  34575  19.9alt  34774  cvrval2  35083  cvrnbtwn2  35084  cvrnbtwn4  35088  hlateq  35207  islpln5  35343  islvol5  35387  pmap11  35570  4atex  35884  cdleme0ex2N  36033  cdlemefrs29pre00  36204  diaord  36857  dihmeetlem13N  37129  lcfl1  37302  lcfls1N  37345  mapdpglem3  37485  isnacs2  37795  mrefg3  37797  pw2f1ocnv  38130  acsfn1p  38295  relexp0eq  38519  frege124d  38579  uneqsn  38847  k0004lem1  38971  sbcoreleleq  39270  dffo3f  39884  climreeq  40363  funressnfv  41728  fmtnorec2lem  41982
  Copyright terms: Public domain W3C validator