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

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

Proof of Theorem bitr2i
StepHypRef Expression
1 bitr2i.1 . . 3 (φψ)
2 bitr2i.2 . . 3 (ψχ)
31, 2bitri 173 . 2 (φχ)
43bicomi 123 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  3bitr2ri  198  3bitr4ri  202  nan  625  pm4.15  788  3or6  1217  sbal1yz  1874  2exsb  1882  moanim  1971  2eu4  1990  cvjust  2032  abbi  2148  sbc8g  2765  ss2rab  3010  unass  3094  unss  3111  undi  3179  difindiss  3185  disj  3262  unopab  3827  eqvinop  3971  pwexb  4172  dmun  4485  reldm0  4496  dmres  4575  imadmrn  4621  ssrnres  4706  dmsnm  4729  coundi  4765  coundir  4766  cnvpom  4803  xpcom  4807  fun11  4909  fununi  4910  funcnvuni  4911  isarep1  4928  fsn  5278  fconstfvm  5322  eufnfv  5332  acexmidlem2  5452  eloprabga  5533  funoprabg  5542  ralrnmpt2  5557  rexrnmpt2  5558  oprabrexex2  5699  dfer2  6043  euen1b  6219  xpsnen  6231
  Copyright terms: Public domain W3C validator