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  682  pm4.15  684  3or6  1302  sbal1yz  1977  2exsb  1985  moanim  2074  2eu4  2093  cvjust  2135  abbi  2254  sbc8g  2919  ss2rab  3177  unass  3237  unss  3254  undi  3328  difindiss  3334  notm0  3387  disj  3415  unopab  4014  eqvinop  4172  pwexb  4402  dmun  4753  reldm0  4764  dmres  4847  imadmrn  4898  ssrnres  4988  dmsnm  5011  coundi  5047  coundir  5048  cnvpom  5088  xpcom  5092  fun11  5197  fununi  5198  funcnvuni  5199  isarep1  5216  fsn  5599  fconstfvm  5645  eufnfv  5655  acexmidlem2  5778  eloprabga  5865  funoprabg  5877  ralrnmpo  5892  rexrnmpo  5893  oprabrexex2  6035  dfer2  6437  euen1b  6704  xpsnen  6722  rexuz3  10793  tgval2  12257  ssntr  12328  metrest  12712  sinhalfpilem  12918
 Copyright terms: Public domain W3C validator