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

Theorem bibi12i 307
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 305 . 2  |-  ( (
ph 
<->  ch )  <->  ( ph  <->  th ) )
3 bibi.a . . 3  |-  ( ph  <->  ps )
43bibi1i 306 . 2  |-  ( (
ph 
<->  th )  <->  ( ps  <->  th ) )
52, 4bitri 241 1  |-  ( (
ph 
<->  ch )  <->  ( ps  <->  th ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  pm5.32  618  orbidi  899  pm5.7  901  xorbi12i  1323  nfnid  4385  asymref  5242  isocnv2  6043  zfcndrep  8481  brsymdif  25665  brtxpsd  25731  f1omvdco3  27350
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 178
  Copyright terms: Public domain W3C validator