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

Theorem bibi12i 306
Description: The equivalence of two equivalences. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bibi.a  |-  ( ph  <->  ps )
bibi12.2  |-  ( ch  <->  th )
Assertion
Ref Expression
bibi12i  |-  ( (
ph 
<->  ch )  <->  ( ps  <->  th ) )

Proof of Theorem bibi12i
StepHypRef Expression
1 bibi12.2 . . 3  |-  ( ch  <->  th )
21bibi2i 304 . 2  |-  ( (
ph 
<->  ch )  <->  ( ph  <->  th ) )
3 bibi.a . . 3  |-  ( ph  <->  ps )
43bibi1i 305 . 2  |-  ( (
ph 
<->  th )  <->  ( ps  <->  th ) )
52, 4bitri 240 1  |-  ( (
ph 
<->  ch )  <->  ( ps  <->  th ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  pm5.32  617  orbidi  898  pm5.7  900  xorbi12i  1305  nfnid  4204  asymref  5059  isocnv2  5828  zfcndrep  8236  brsymdif  24372  brtxpsd  24434  isoriso  25212  f1omvdco3  27392  compneOLD  27643
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