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  732  excxor  1254  sbequ8  1709  2sb5  1841  2sb6  1842  2sb5rf  1847  2sb6rf  1848  moabs  1931  moanim  1956  2eu4  1975  2eu7  1976  sb8ab  2141  risset  2330  reuind  2721  difundi  3166  indifdir  3170  unab  3181  inab  3182  rabeq0  3224  abeq0  3225  inssdif0im  3268  snprc  3409  snss  3468  unipr  3568  uni0b  3579  pwtr  3929  opm  3945  elxp2  4290  opthprc  4318  xpiundir  4326  elvvv  4330  relun  4381  inopab  4395  difopab  4396  ralxpf  4409  rexxpf  4410  dmiun  4471  rniun  4661  cnvresima  4737  imaco  4753  fnopabg  4948  dff1o2  5056  idref  5321  imaiun  5324  opabex3d  5671  opabex3  5672  dcnbidcnn  7006  alsconv  7211
  Copyright terms: Public domain W3C validator