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  4220  asymref  5075  isocnv2  5844  zfcndrep  8252  brsymdif  24443  brtxpsd  24505  isoriso  25315  f1omvdco3  27495  compneOLD  27746
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