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

Theorem bibi1i 321
Description: Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
bibi2i.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
bibi1i  |-  ( (
ph 
<->  ch )  <->  ( ps  <->  ch ) )

Proof of Theorem bibi1i
StepHypRef Expression
1 bicom 205 . 2  |-  ( (
ph 
<->  ch )  <->  ( ch  <->  ph ) )
2 bibi2i.1 . . 3  |-  ( ph  <->  ps )
32bibi2i 320 . 2  |-  ( ( ch  <->  ph )  <->  ( ch  <->  ps ) )
4 bicom 205 . 2  |-  ( ( ch  <->  ps )  <->  ( ps  <->  ch ) )
51, 3, 43bitri 279 1  |-  ( (
ph 
<->  ch )  <->  ( ps  <->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189
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 190
This theorem is referenced by:  bibi12i  322  biluk  947  xorass  1434  xorassOLD  1435  hadbi  1509  hadnot  1513  sbrbis  2254  ssequn1  3595  symdifass  3663  asymref  5222  aceq1  8566  aceq0  8567  zfac  8908  zfcndac  9062  funcnvmptOLD  28345  axacprim  30406  rp-fakeanorass  36228  rp-fakenanass  36230
  Copyright terms: Public domain W3C validator