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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  dcnnOLD  817  excxor  1339  sbequ8  1801  2sb5  1934  2sb6  1935  2sb5rf  1940  2sb6rf  1941  moabs  2024  moanim  2049  2eu4  2068  2eu7  2069  sb8ab  2236  risset  2437  reuind  2858  difundi  3294  indifdir  3298  unab  3309  inab  3310  rabeq0  3358  abeq0  3359  inssdif0im  3396  snprc  3554  snss  3615  unipr  3716  uni0b  3727  pwtr  4101  opm  4116  onintexmid  4447  elxp2  4517  opthprc  4550  xpiundir  4558  elvvv  4562  relun  4616  inopab  4631  difopab  4632  ralxpf  4645  rexxpf  4646  dmiun  4708  rniun  4907  cnvresima  4986  imaco  5002  fnopabg  5204  dff1o2  5328  idref  5612  imaiun  5615  opabex3d  5973  opabex3  5974  elixx3g  9577  elfz2  9690  elfzuzb  9693  divalgb  11470  1nprm  11641  alsconv  12937
  Copyright terms: Public domain W3C validator