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  1494  hadnot  1498  sbrbis  2204  ssequn1  3572  symdifass  3638  asymref  5171  aceq1  8492  aceq0  8493  zfac  8834  zfcndac  8988  funcnvmptOLD  28209  axacprim  30279  rp-fakeanorass  36064  rp-fakenanass  36066
  Copyright terms: Public domain W3C validator