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

Theorem bitr2i 184
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 183 . 2 (𝜑𝜒)
43bicomi 131 1 (𝜒𝜑)
Colors of variables: wff set class
Syntax hints:  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3bitrri  206  3bitr2ri  208  3bitr4ri  212  nan  666  pm4.15  668  3or6  1286  sbal1yz  1954  2exsb  1962  moanim  2051  2eu4  2070  cvjust  2112  abbi  2231  sbc8g  2889  ss2rab  3143  unass  3203  unss  3220  undi  3294  difindiss  3300  notm0  3353  disj  3381  unopab  3977  eqvinop  4135  pwexb  4365  dmun  4716  reldm0  4727  dmres  4810  imadmrn  4861  ssrnres  4951  dmsnm  4974  coundi  5010  coundir  5011  cnvpom  5051  xpcom  5055  fun11  5160  fununi  5161  funcnvuni  5162  isarep1  5179  fsn  5560  fconstfvm  5606  eufnfv  5616  acexmidlem2  5739  eloprabga  5826  funoprabg  5838  ralrnmpo  5853  rexrnmpo  5854  oprabrexex2  5996  dfer2  6398  euen1b  6665  xpsnen  6683  rexuz3  10730  tgval2  12147  ssntr  12218  metrest  12602  sinhalfpilem  12799
  Copyright terms: Public domain W3C validator