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  2415  necon2bbid  2834  fressnfv  6412  eluniima  6493  dfac2  8938  alephval2  9379  adderpqlem  9761  1idpr  9836  leloe  10109  negeq0  10320  muleqadd  10656  addltmul  11253  xrleloe  11962  fzrev  12388  mod0  12658  modirr  12724  cjne0  13884  lenegsq  14041  fsumsplit  14452  sumsplit  14480  dvdsabseq  15016  xpsfrnel  16204  isacs2  16295  acsfn  16301  comfeq  16347  sgrp2nmndlem3  17393  resscntz  17745  gexdvds  17980  hauscmplem  21190  hausdiag  21429  utop3cls  22036  ltgov  25473  ax5seglem4  25793  mdsl2i  29151  addeq0  29484  pl1cn  29975  topdifinfeq  33169  finxpreclem6  33204  ftc1anclem5  33460  fdc1  33513  lcvexchlem1  34140  lkreqN  34276  glbconxN  34483  islpln5  34640  islvol5  34684  cdlemefrs29bpre0  35503  cdlemg17h  35775  cdlemg33b  35814  brnonrel  37714  frege92  38069  e2ebind  38599  stoweidlem28  40008
  Copyright terms: Public domain W3C validator