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  2026  ssequn1  3358  asymref  5075  aceq1  7760  aceq0  7761  zfac  8102  zfcndac  8257  or3dir  23140  funcnvmptOLD  23249  funcnvmpt  23250  measvuni  23557  axacprim  24068  symdifass  24442  difeqri2  25143  compneOLD  27746  sbrbisNEW7  29613
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