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

Theorem 3bitr4ri 212
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 186 . 2 (𝜑𝜃)
51, 4bitr2i 184 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:  dcnnOLD  819  excxor  1341  sbequ8  1803  2sb5  1936  2sb6  1937  2sb5rf  1942  2sb6rf  1943  moabs  2026  moanim  2051  2eu4  2070  2eu7  2071  sb8ab  2239  risset  2440  reuind  2862  difundi  3298  indifdir  3302  unab  3313  inab  3314  rabeq0  3362  abeq0  3363  inssdif0im  3400  snprc  3558  snss  3619  unipr  3720  uni0b  3731  pwtr  4111  opm  4126  onintexmid  4457  elxp2  4527  opthprc  4560  xpiundir  4568  elvvv  4572  relun  4626  inopab  4641  difopab  4642  ralxpf  4655  rexxpf  4656  dmiun  4718  rniun  4919  cnvresima  4998  imaco  5014  fnopabg  5216  dff1o2  5340  idref  5626  imaiun  5629  opabex3d  5987  opabex3  5988  elixx3g  9652  elfz2  9765  elfzuzb  9768  divalgb  11549  1nprm  11722  alsconv  13173
  Copyright terms: Public domain W3C validator