ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr4ri 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  823  excxor  1269  sbequ8  1727  2sb5  1859  2sb6  1860  2sb5rf  1865  2sb6rf  1866  moabs  1949  moanim  1974  2eu4  1993  2eu7  1994  sb8ab  2159  risset  2352  reuind  2744  difundi  3189  indifdir  3193  unab  3204  inab  3205  rabeq0  3247  abeq0  3248  inssdif0im  3291  snprc  3435  snss  3494  unipr  3594  uni0b  3605  pwtr  3955  opm  3971  onintexmid  4297  elxp2  4363  opthprc  4391  xpiundir  4399  elvvv  4403  relun  4454  inopab  4468  difopab  4469  ralxpf  4482  rexxpf  4483  dmiun  4544  rniun  4734  cnvresima  4810  imaco  4826  fnopabg  5022  dff1o2  5131  idref  5396  imaiun  5399  opabex3d  5748  opabex3  5749  elixx3g  8768  elfz2  8879  elfzuzb  8882  alsconv  10092
  Copyright terms: Public domain W3C validator