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

Theorem 3bitr2i 207
 Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr2i.1 (𝜑𝜓)
3bitr2i.2 (𝜒𝜓)
3bitr2i.3 (𝜒𝜃)
Assertion
Ref Expression
3bitr2i (𝜑𝜃)

Proof of Theorem 3bitr2i
StepHypRef Expression
1 3bitr2i.1 . . 3 (𝜑𝜓)
2 3bitr2i.2 . . 3 (𝜒𝜓)
31, 2bitr4i 186 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitri 183 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:  an13  552  sbanv  1861  sbexyz  1978  exists1  2095  euxfrdc  2870  euind  2871  rmo4  2877  rmo3f  2881  rmo3  3000  ddifstab  3208  opm  4156  uniuni  4372  rabxp  4576  eliunxp  4678  dmmrnm  4758  imadisj  4901  intirr  4925  resco  5043  funcnv3  5185  fncnv  5189  fun11  5190  fununi  5191  f1mpt  5672  mpomptx  5862  ixp0x  6620  mapsnen  6705  xpcomco  6720  enq0tr  7242  elq  9414  ntreq0  12301  tx1cn  12438
 Copyright terms: Public domain W3C validator