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

Theorem bitr2i 183
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 182 . 2 (𝜑𝜒)
43bicomi 130 1 (𝜒𝜑)
Colors of variables: wff set class
Syntax hints:  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3bitrri  205  3bitr2ri  207  3bitr4ri  211  nan  661  pm4.15  827  3or6  1259  sbal1yz  1925  2exsb  1933  moanim  2022  2eu4  2041  cvjust  2083  abbi  2201  sbc8g  2845  ss2rab  3095  unass  3155  unss  3172  undi  3245  difindiss  3251  notm0  3301  disj  3328  unopab  3909  eqvinop  4061  pwexb  4287  dmun  4631  reldm0  4642  dmres  4721  imadmrn  4771  ssrnres  4860  dmsnm  4883  coundi  4919  coundir  4920  cnvpom  4960  xpcom  4964  fun11  5067  fununi  5068  funcnvuni  5069  isarep1  5086  fsn  5453  fconstfvm  5497  eufnfv  5507  acexmidlem2  5631  eloprabga  5717  funoprabg  5726  ralrnmpt2  5741  rexrnmpt2  5742  oprabrexex2  5883  dfer2  6273  euen1b  6500  xpsnen  6517  rexuz3  10388
  Copyright terms: Public domain W3C validator