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

Theorem syl6rbbr 281
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 215 . 2 (𝜒𝜃)
41, 3syl6rbb 279 1 (𝜑 → (𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  baib  531  cad1  1725  necon2abid  2979  reueubd  3312  reu8  3561  sbc6g  3622  r19.28z  4222  r19.37zv  4226  r19.45zv  4227  r19.44zv  4228  r19.27z  4229  r19.36zv  4231  ralidm  4234  ralsnsg  4373  eldifvsn  4482  ssunsn2  4512  iunconst  4685  iinconst  4686  relsng  5392  opelres  5571  ordsseleq  5937  ordequn  6008  funssres  6111  fncnv  6140  fresaun  6257  dff1o5  6329  funimass4  6436  fndmdifeq0  6513  fneqeql2  6516  unpreima  6531  dffo3  6564  fnnfpeq0  6637  funfvima  6685  f1eqcocnv  6748  fliftf  6757  isocnv3  6774  isomin  6779  eloprabga  6945  mpt22eqb  6967  elpwun  7175  dfom2  7265  opabex3d  7343  opabex3  7344  f1oweALT  7350  fnwelem  7494  mptsuppd  7520  dfrecs3  7673  oe0m1  7806  oarec  7847  boxcutc  8156  ordunifi  8417  r1fin  8851  rankr1c  8899  iscard  9052  iscard2  9053  cardval2  9068  dfac3  9195  kmlem8  9232  infinf  9641  xrlenlt  10357  ltxrlt  10362  negcon2  10588  mulne0b  10922  dfinfre  11258  crne0  11267  elznn  11640  zmax  11986  zq  11995  elfznelfzo  12781  modmuladdnn0  12922  hashneq0  13357  xpcogend  14002  sqrtneglem  14294  rexfiuz  14374  rexanuz2  14376  sumsplit  14786  fsum2dlem  14788  odd2np1  15349  divalgb  15411  gcdcllem2  15505  mrcidb2  16546  fncnvimaeqv  17027  lbsacsbs  19430  islpir2  19525  domnmuln0  19572  mplcoe1  19739  mplcoe5  19742  islinds2  20428  islbs4  20447  mamucl  20483  mavmulcl  20630  mdetunilem8  20702  iscld4  21149  isconn2  21497  kgencn  21639  tx1cn  21692  tx2cn  21693  elmptrab  21910  isfbas  21912  fbfinnfr  21924  cnfcf  22125  fmucndlem  22374  prdsxmslem2  22613  blval2  22646  cnbl0  22856  cnblcld  22857  metcld  23383  ismbf  23686  ismbfcn  23687  itg1val2  23742  itg2split  23807  itg2monolem1  23808  aannenlem1  24374  pilem1  24496  sinq34lt0t  24553  ellogrn  24597  logeftb  24621  gausslemma2dlem1a  25381  ercgrg  25703  usgredgffibi  26495  vtxd0nedgb  26675  vdiscusgrb  26717  upgrspthswlk  26925  s3wwlks2on  27160  frgrncvvdeqlem2  27538  ch0pss  28695  h1de2ctlem  28805  adjsym  29083  eigposi  29086  dfadj2  29135  elnlfn  29178  xppreima  29834  1stpreima  29868  2ndpreima  29869  qtophaus  30285  prsdm  30342  prsrn  30343  1stmbfm  30704  2ndmbfm  30705  eulerpartlemn  30825  reprdifc  31088  circlemeth  31101  bnj1454  31292  bnj984  31402  elintfv  32039  dffun10  32397  hfext  32666  isfne4b  32711  neifg  32741  taupilem3  33531  topdifinfindis  33559  topdifinffinlem  33560  finxpsuclem  33599  poimirlem23  33788  poimirlem26  33791  cnambfre  33813  0totbnd  33926  opelvvdif  34390  inecmo  34481  brxrn  34497  brin2  34528  eleccossin  34594  cvrval2  35162  cvrnbtwn2  35163  cvrnbtwn4  35167  hlateq  35287  islpln5  35423  islvol5  35467  pmap11  35650  4atex  35964  cdleme0ex2N  36112  cdlemefrs29pre00  36283  diaord  36935  dihmeetlem13N  37207  lcfl1  37380  lcfls1N  37423  mapdpglem3  37563  isnacs2  37879  mrefg3  37881  pw2f1ocnv  38213  acsfn1p  38378  relexp0eq  38600  frege124d  38660  uneqsn  38927  k0004lem1  39051  sbcoreleleq  39345  dffo3f  39943  climreeq  40415  funressnfv  41752  fmtnorec2lem  42062
  Copyright terms: Public domain W3C validator