ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bitr3i Structured version   GIF 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  509  anandir  510  xchnxbi  589  orordi  674  orordir  675  sbco3v  1819  elsb3  1828  elsb4  1829  sbco4  1859  abeq1i  2125  r19.41  2437  rexcom4a  2549  moeq  2687  mosubt  2689  2reuswapdc  2714  nfcdeq  2732  sbcid  2750  sbcco2  2757  sbc7  2761  sbcie2g  2767  eqsbc3  2773  sbcralt  2805  sbcrext  2806  cbvralcsf  2879  cbvrexcsf  2880  cbvrabcsf  2882  abss  2980  ssab  2981  difrab  3182  prsspw  3502  brab1  3775  unopab  3802  exss  3929  uniuni  4124  elvvv  4321  eliunxp  4393  ralxp  4397  rexxp  4398  opelco  4425  reldm0  4471  resieq  4540  resiexg  4571  iss  4572  imai  4599  cnvsym  4626  intasym  4627  asymref  4628  codir  4631  poirr2  4635  rninxp  4682  cnvsom  4779  funopg  4851  fin  4992  f1cnvcnv  5016  fndmin  5190  resoprab  5511  mpt22eqb  5524  ov6g  5552  offval  5633  dfopab2  5729  dfoprab3s  5730  fmpt2x  5740  brtpos0  5780  dftpos3  5790  tpostpos  5792  frec0g  5893  ercnv  6029  elni2  6163
  Copyright terms: Public domain W3C validator