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

Theorem syl5rbbr 287
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 225 . 2 (𝜑𝜓)
3 syl5rbbr.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5rbb 285 1 (𝜒 → (𝜃𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  sbco3  2553  necon2bbid  3064  notzfaus  5259  fressnfv  6920  eluniima  7005  dfac2b  9550  alephval2  9988  adderpqlem  10370  1idpr  10445  leloe  10721  negeq0  10934  addeq0  11057  muleqadd  11278  addltmul  11867  xrleloe  12532  fzrev  12965  mod0  13239  modirr  13305  cjne0  14517  lenegsq  14675  fsumsplit  15092  sumsplit  15118  dvdsabseq  15658  xpsfrnel  16830  isacs2  16919  acsfn  16925  comfeq  16971  sgrp2nmndlem3  18035  resscntz  18407  gexdvds  18645  hauscmplem  21949  hausdiag  22188  utop3cls  22794  affineequivne  25337  ltgov  26316  ax5seglem4  26651  mdsl2i  30032  rspc2daf  30164  cycpmco2  30708  pl1cn  31103  satefvfmla1  32575  topdifinfeq  34519  finxpreclem6  34565  ftc1anclem5  34857  fdc1  34908  relcnveq  35466  relcnveq2  35467  elrelscnveq  35618  elrelscnveq2  35619  lcvexchlem1  36056  lkreqN  36192  glbconxN  36400  islpln5  36557  islvol5  36601  cdlemefrs29bpre0  37418  cdlemg17h  37690  cdlemg33b  37729  brnonrel  39833  frege92  40185  e2ebind  40781  stoweidlem28  42198
  Copyright terms: Public domain W3C validator