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

Theorem bibi1i 306
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 192 . 2  |-  ( (
ph 
<->  ch )  <->  ( ch  <->  ph ) )
2 bibi.a . . 3  |-  ( ph  <->  ps )
32bibi2i 305 . 2  |-  ( ( ch  <->  ph )  <->  ( ch  <->  ps ) )
4 bicom 192 . 2  |-  ( ( ch  <->  ps )  <->  ( ps  <->  ch ) )
51, 3, 43bitri 263 1  |-  ( (
ph 
<->  ch )  <->  ( ps  <->  ch ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  bibi12i  307  biluk  900  xorass  1317  hadbi  1396  sbrbis  2145  ssequn1  3517  asymref  5250  aceq1  7998  aceq0  7999  zfac  8340  zfcndac  8494  funcnvmptOLD  24082  axacprim  25156  symdifass  25672  sbrbisNEW7  29642
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 178
  Copyright terms: Public domain W3C validator