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  613  pm4.15  782  3or6  1203  sbal1yz  1859  2exsb  1867  moanim  1956  2eu4  1975  cvjust  2017  abbi  2133  sbc8g  2748  ss2rab  2993  unass  3077  unss  3094  undi  3162  difindiss  3168  disj  3245  unopab  3810  eqvinop  3954  pwexb  4156  dmun  4469  reldm0  4480  dmres  4559  imadmrn  4605  ssrnres  4690  dmsnm  4713  coundi  4749  coundir  4750  cnvpom  4787  xpcom  4791  fun11  4892  fununi  4893  funcnvuni  4894  isarep1  4911  fsn  5260  fconstfvm  5304  eufnfv  5314  acexmidlem2  5433  eloprabga  5514  funoprabg  5523  ralrnmpt2  5538  rexrnmpt2  5539  oprabrexex2  5680  dfer2  6018
  Copyright terms: Public domain W3C validator