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

Theorem bitr3i 175
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr3i.1
bitr3i.2
Assertion
Ref Expression
bitr3i

Proof of Theorem bitr3i
StepHypRef Expression
1 bitr3i.1 . . 3
21bicomi 123 . 2
3 bitr3i.2 . 2
42, 3bitri 173 1
Colors of variables: wff set class
Syntax hints:   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  3bitrri  196  3bitr3i  199  3bitr3ri  200  anandi  524  anandir  525  xchnxbi  604  orordi  689  orordir  690  sbco3v  1840  elsb3  1849  elsb4  1850  sbco4  1880  abeq1i  2146  r19.41  2459  rexcom4a  2572  moeq  2710  mosubt  2712  2reuswapdc  2737  nfcdeq  2755  sbcid  2773  sbcco2  2780  sbc7  2784  sbcie2g  2790  eqsbc3  2796  sbcralt  2828  sbcrext  2829  cbvralcsf  2902  cbvrexcsf  2903  cbvrabcsf  2905  abss  3003  ssab  3004  difrab  3205  prsspw  3527  brab1  3800  unopab  3827  exss  3954  uniuni  4149  elvvv  4346  eliunxp  4418  ralxp  4422  rexxp  4423  opelco  4450  reldm0  4496  resieq  4565  resiexg  4596  iss  4597  imai  4624  cnvsym  4651  intasym  4652  asymref  4653  codir  4656  poirr2  4660  rninxp  4707  cnvsom  4804  funopg  4877  fin  5019  f1cnvcnv  5043  fndmin  5217  resoprab  5539  mpt22eqb  5552  ov6g  5580  offval  5661  dfopab2  5757  dfoprab3s  5758  fmpt2x  5768  brtpos0  5808  dftpos3  5818  tpostpos  5820  ercnv  6063  xpcomco  6236  xpassen  6240  elni2  6298  elfz2nn0  8723  elfzmlbp  8740  expival  8891
  Copyright terms: Public domain W3C validator