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

Theorem 3bitr4ri 211
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 185 . 2 (𝜑𝜃)
51, 4bitr2i 183 1 (𝜃𝜒)
Colors of variables: wff set class
Syntax hints:  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  testbitestn  859  excxor  1312  sbequ8  1772  2sb5  1904  2sb6  1905  2sb5rf  1910  2sb6rf  1911  moabs  1994  moanim  2019  2eu4  2038  2eu7  2039  sb8ab  2206  risset  2402  reuind  2809  difundi  3240  indifdir  3244  unab  3255  inab  3256  rabeq0  3301  abeq0  3302  inssdif0im  3338  snprc  3490  snss  3549  unipr  3650  uni0b  3661  pwtr  4020  opm  4035  onintexmid  4361  elxp2  4429  opthprc  4457  xpiundir  4465  elvvv  4469  relun  4522  inopab  4536  difopab  4537  ralxpf  4550  rexxpf  4551  dmiun  4613  rniun  4808  cnvresima  4886  imaco  4902  fnopabg  5102  dff1o2  5221  idref  5497  imaiun  5500  opabex3d  5849  opabex3  5850  elixx3g  9251  elfz2  9363  elfzuzb  9366  divalgb  10800  1nprm  10971  alsconv  11359
  Copyright terms: Public domain W3C validator