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

Theorem bibi1i 315
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 203 . 2  |-  ( (
ph 
<->  ch )  <->  ( ch  <->  ph ) )
2 bibi2i.1 . . 3  |-  ( ph  <->  ps )
32bibi2i 314 . 2  |-  ( ( ch  <->  ph )  <->  ( ch  <->  ps ) )
4 bicom 203 . 2  |-  ( ( ch  <->  ps )  <->  ( ps  <->  ch ) )
51, 3, 43bitri 274 1  |-  ( (
ph 
<->  ch )  <->  ( ps  <->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187
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 188
This theorem is referenced by:  bibi12i  316  biluk  941  xorass  1404  xorassOLD  1405  hadbi  1496  hadnot  1500  sbrbis  2200  ssequn1  3642  symdifass  3708  asymref  5236  aceq1  8546  aceq0  8547  zfac  8888  zfcndac  9043  funcnvmptOLD  28110  axacprim  30122  rp-fakeanorass  35856  rp-fakenanass  35858
  Copyright terms: Public domain W3C validator