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

Theorem syl5rbbr 278
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 216 . 2 (𝜑𝜓)
3 syl5rbbr.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5rbb 276 1 (𝜒 → (𝜃𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198
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 199
This theorem is referenced by:  sbco3  2535  necon2bbid  3013  fressnfv  6654  eluniima  6735  dfac2b  9238  dfac2OLD  9240  alephval2  9681  adderpqlem  10063  1idpr  10138  leloe  10413  negeq0  10626  muleqadd  10962  addltmul  11553  xrleloe  12221  fzrev  12654  mod0  12927  modirr  12993  cjne0  14241  lenegsq  14398  fsumsplit  14809  sumsplit  14835  dvdsabseq  15371  xpsfrnel  16535  isacs2  16625  acsfn  16631  comfeq  16677  sgrp2nmndlem3  17725  resscntz  18073  gexdvds  18309  hauscmplem  21535  hausdiag  21774  utop3cls  22380  ltgov  25841  ax5seglem4  26162  mdsl2i  29699  addeq0  30021  pl1cn  30510  topdifinfeq  33689  finxpreclem6  33724  ftc1anclem5  33970  fdc1  34022  relcnveq  34580  relcnveq2  34581  elrelscnveq  34729  elrelscnveq2  34730  lcvexchlem1  35048  lkreqN  35184  glbconxN  35392  islpln5  35549  islvol5  35593  cdlemefrs29bpre0  36410  cdlemg17h  36682  cdlemg33b  36721  brnonrel  38667  frege92  39020  e2ebind  39538  stoweidlem28  40977
  Copyright terms: Public domain W3C validator