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  511  anandir  512  xchnxbi  592  orordi  677  orordir  678  sbco3v  1825  elsb3  1834  elsb4  1835  sbco4  1865  abeq1i  2131  r19.41  2443  rexcom4a  2555  moeq  2693  mosubt  2695  2reuswapdc  2720  nfcdeq  2738  sbcid  2756  sbcco2  2763  sbc7  2767  sbcie2g  2773  eqsbc3  2779  sbcralt  2811  sbcrext  2812  cbvralcsf  2885  cbvrexcsf  2886  cbvrabcsf  2888  abss  2986  ssab  2987  difrab  3188  prsspw  3510  brab1  3783  unopab  3810  exss  3937  uniuni  4133  elvvv  4330  eliunxp  4402  ralxp  4406  rexxp  4407  opelco  4434  reldm0  4480  resieq  4549  resiexg  4580  iss  4581  imai  4608  cnvsym  4635  intasym  4636  asymref  4637  codir  4640  poirr2  4644  rninxp  4691  cnvsom  4788  funopg  4860  fin  5001  f1cnvcnv  5025  fndmin  5199  resoprab  5520  mpt22eqb  5533  ov6g  5561  offval  5642  dfopab2  5738  dfoprab3s  5739  fmpt2x  5749  brtpos0  5789  dftpos3  5799  tpostpos  5801  frec0g  5902  ercnv  6038  elni2  6174
  Copyright terms: Public domain W3C validator