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

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

Proof of Theorem bitr3di
StepHypRef Expression
1 bitr3di.2 . . 3 (𝜓𝜃)
21bicomi 227 . 2 (𝜃𝜓)
3 bitr3di.1 . 2 (𝜑 → (𝜓𝜒))
42, 3syl5rbb 287 1 (𝜑 → (𝜒𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  sbco3  2532  necon2bbid  3030  notzfaus  5227  fressnfv  6899  eluniima  6987  dfac2b  9543  alephval2  9985  adderpqlem  10367  1idpr  10442  leloe  10718  negeq0  10931  addeq0  11054  muleqadd  11275  addltmul  11863  xrleloe  12527  fzrev  12967  mod0  13241  modirr  13307  cjne0  14516  lenegsq  14674  fsumsplit  15091  sumsplit  15117  dvdsabseq  15657  xpsfrnel  16829  isacs2  16918  acsfn  16924  comfeq  16970  sgrp2nmndlem3  18084  resscntz  18457  gexdvds  18704  hauscmplem  22018  hausdiag  22257  utop3cls  22864  affineequivne  25420  ltgov  26398  ax5seglem4  26733  mdsl2i  30112  rspc2daf  30245  cycpmco2  30832  pl1cn  31320  satefvfmla1  32797  topdifinfeq  34783  finxpreclem6  34829  ftc1anclem5  35150  fdc1  35200  relcnveq  35755  relcnveq2  35756  elrelscnveq  35908  elrelscnveq2  35909  lcvexchlem1  36346  lkreqN  36482  glbconxN  36690  islpln5  36847  islvol5  36891  cdlemefrs29bpre0  37708  cdlemg17h  37980  cdlemg33b  38019  brnonrel  40304  frege92  40671  e2ebind  41284  stoweidlem28  42685
 Copyright terms: Public domain W3C validator