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

Theorem 3bitr4ri 202
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)
Hypotheses
Ref Expression
3bitr4i.1 (φψ)
3bitr4i.2 (χφ)
3bitr4i.3 (θψ)
Assertion
Ref Expression
3bitr4ri (θχ)

Proof of Theorem 3bitr4ri
StepHypRef Expression
1 3bitr4i.2 . 2 (χφ)
2 3bitr4i.1 . . 3 (φψ)
3 3bitr4i.3 . . 3 (θψ)
42, 3bitr4i 176 . 2 (φθ)
51, 4bitr2i 174 1 (θχ)
Colors of variables: wff set class
Syntax hints:  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  testbitestn  822  excxor  1268  sbequ8  1724  2sb5  1856  2sb6  1857  2sb5rf  1862  2sb6rf  1863  moabs  1946  moanim  1971  2eu4  1990  2eu7  1991  sb8ab  2156  risset  2346  reuind  2738  difundi  3183  indifdir  3187  unab  3198  inab  3199  rabeq0  3241  abeq0  3242  inssdif0im  3285  snprc  3426  snss  3485  unipr  3585  uni0b  3596  pwtr  3946  opm  3962  elxp2  4306  opthprc  4334  xpiundir  4342  elvvv  4346  relun  4397  inopab  4411  difopab  4412  ralxpf  4425  rexxpf  4426  dmiun  4487  rniun  4677  cnvresima  4753  imaco  4769  fnopabg  4965  dff1o2  5074  idref  5339  imaiun  5342  opabex3d  5690  opabex3  5691  elixx3g  8500  elfz2  8611  elfzuzb  8614  alsconv  9377
  Copyright terms: Public domain W3C validator