ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bitr3i Unicode version

Theorem bitr3i 184
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr3i.1  |-  ( ps  <->  ph )
bitr3i.2  |-  ( ps  <->  ch )
Assertion
Ref Expression
bitr3i  |-  ( ph  <->  ch )

Proof of Theorem bitr3i
StepHypRef Expression
1 bitr3i.1 . . 3  |-  ( ps  <->  ph )
21bicomi 130 . 2  |-  ( ph  <->  ps )
3 bitr3i.2 . 2  |-  ( ps  <->  ch )
42, 3bitri 182 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3bitrri  205  3bitr3i  208  3bitr3ri  209  anandi  557  anandir  558  xchnxbi  640  orordi  725  orordir  726  sbco3v  1891  elsb3  1900  elsb4  1901  sbco4  1931  abeq1i  2199  r19.41  2522  rexcom4a  2643  moeq  2788  mosubt  2790  2reuswapdc  2817  nfcdeq  2835  sbcid  2853  sbcco2  2860  sbc7  2864  sbcie2g  2870  eqsbc3  2876  sbcralt  2913  sbcrext  2914  cbvralcsf  2988  cbvrexcsf  2989  cbvrabcsf  2991  abss  3088  ssab  3089  difrab  3271  abn0m  3306  prsspw  3604  disjnim  3828  brab1  3882  unopab  3909  exss  4045  uniuni  4264  elvvv  4489  eliunxp  4563  ralxp  4567  rexxp  4568  opelco  4596  reldm0  4642  resieq  4711  resiexg  4744  iss  4745  imai  4775  cnvsym  4802  intasym  4803  asymref  4804  codir  4807  poirr2  4811  rninxp  4861  cnvsom  4961  funopg  5034  fin  5181  f1cnvcnv  5211  fndmin  5390  resoprab  5723  mpt22eqb  5736  ov6g  5764  offval  5845  dfopab2  5941  dfoprab3s  5942  fmpt2x  5952  spc2ed  5980  brtpos0  5999  dftpos3  6009  tpostpos  6011  ercnv  6293  xpcomco  6522  xpassen  6526  phpm  6561  elni2  6852  elfz2nn0  9493  elfzmlbp  9508  clim0  10637
  Copyright terms: Public domain W3C validator