ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bitr3di Unicode version

Theorem bitr3di 194
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
Hypotheses
Ref Expression
bitr3di.1  |-  ( ph  ->  ( ps  <->  ch )
)
bitr3di.2  |-  ( ps  <->  th )
Assertion
Ref Expression
bitr3di  |-  ( ph  ->  ( ch  <->  th )
)

Proof of Theorem bitr3di
StepHypRef Expression
1 bitr3di.2 . . 3  |-  ( ps  <->  th )
21bicomi 131 . 2  |-  ( th  <->  ps )
3 bitr3di.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3syl5rbb 192 1  |-  ( ph  ->  ( ch  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  xordc  1370  sbal2  1997  eqsnm  3682  fnressn  5606  fressnfv  5607  eluniimadm  5666  genpassl  7344  genpassu  7345  1idprl  7410  1idpru  7411  axcaucvglemres  7719  negeq0  8028  muleqadd  8441  crap0  8728  addltmul  8968  fzrev  9876  modq0  10114  cjap0  10691  cjne0  10692  caucvgrelemrec  10763  lenegsq  10879  isumss  11172  fsumsplit  11188  sumsplitdc  11213  dvdsabseq  11556  oddennn  11916  metrest  12689  elabgf0  13089
  Copyright terms: Public domain W3C validator