MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bibi1i Unicode version

Theorem bibi1i 305
Description: Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
bibi.a  |-  ( ph  <->  ps )
Assertion
Ref Expression
bibi1i  |-  ( (
ph 
<->  ch )  <->  ( ps  <->  ch ) )

Proof of Theorem bibi1i
StepHypRef Expression
1 bicom 191 . 2  |-  ( (
ph 
<->  ch )  <->  ( ch  <->  ph ) )
2 bibi.a . . 3  |-  ( ph  <->  ps )
32bibi2i 304 . 2  |-  ( ( ch  <->  ph )  <->  ( ch  <->  ps ) )
4 bicom 191 . 2  |-  ( ( ch  <->  ps )  <->  ( ps  <->  ch ) )
51, 3, 43bitri 262 1  |-  ( (
ph 
<->  ch )  <->  ( ps  <->  ch ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  bibi12i  306  biluk  899  xorass  1299  hadbi  1377  sbrbis  2013  ssequn1  3345  asymref  5059  aceq1  7744  aceq0  7745  zfac  8086  zfcndac  8241  or3dir  23124  funcnvmptOLD  23234  funcnvmpt  23235  measvuni  23542  axacprim  24053  symdifass  24371  difeqri2  25040  compneOLD  27643
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator