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

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

Proof of Theorem syl5rbbr
StepHypRef Expression
1 syl5rbbr.1 . . 3 (𝜓𝜑)
21bicomi 214 . 2 (𝜑𝜓)
3 syl5rbbr.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5rbb 273 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:  sbco3  2564  necon2bbid  2986  fressnfv  6570  eluniima  6651  dfac2b  9153  dfac2OLD  9155  alephval2  9596  adderpqlem  9978  1idpr  10053  leloe  10326  negeq0  10537  muleqadd  10873  addltmul  11470  xrleloe  12182  fzrev  12610  mod0  12883  modirr  12949  cjne0  14111  lenegsq  14268  fsumsplit  14679  sumsplit  14707  dvdsabseq  15244  xpsfrnel  16431  isacs2  16521  acsfn  16527  comfeq  16573  sgrp2nmndlem3  17620  resscntz  17971  gexdvds  18206  hauscmplem  21430  hausdiag  21669  utop3cls  22275  ltgov  25713  ax5seglem4  26033  mdsl2i  29521  addeq0  29850  pl1cn  30341  topdifinfeq  33535  finxpreclem6  33570  ftc1anclem5  33821  fdc1  33874  relcnveq  34436  relcnveq2  34437  elrelscnveq  34584  elrelscnveq2  34585  lcvexchlem1  34843  lkreqN  34979  glbconxN  35186  islpln5  35343  islvol5  35387  cdlemefrs29bpre0  36205  cdlemg17h  36477  cdlemg33b  36516  brnonrel  38421  frege92  38775  e2ebind  39304  stoweidlem28  40762
  Copyright terms: Public domain W3C validator