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

Theorem bitr2i 178
 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 177 . 2 (𝜑𝜒)
43bicomi 127 1 (𝜒𝜑)
 Colors of variables: wff set class Syntax hints:   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  3bitrri  200  3bitr2ri  202  3bitr4ri  206  nan  636  pm4.15  800  3or6  1229  sbal1yz  1893  2exsb  1901  moanim  1990  2eu4  2009  cvjust  2051  abbi  2167  sbc8g  2793  ss2rab  3043  unass  3127  unss  3144  undi  3212  difindiss  3218  disj  3295  unopab  3863  eqvinop  4007  pwexb  4233  dmun  4569  reldm0  4580  dmres  4659  imadmrn  4705  ssrnres  4790  dmsnm  4813  coundi  4849  coundir  4850  cnvpom  4887  xpcom  4891  fun11  4993  fununi  4994  funcnvuni  4995  isarep1  5012  fsn  5362  fconstfvm  5406  eufnfv  5416  acexmidlem2  5536  eloprabga  5618  funoprabg  5627  ralrnmpt2  5642  rexrnmpt2  5643  oprabrexex2  5784  dfer2  6137  euen1b  6313  xpsnen  6325  rexuz3  9816
 Copyright terms: Public domain W3C validator