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

Theorem 3bitr4ri 206
 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 180 . 2 (𝜑𝜃)
51, 4bitr2i 178 1 (𝜃𝜒)
 Colors of variables: wff set class Syntax hints:   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  testbitestn  834  excxor  1285  sbequ8  1743  2sb5  1875  2sb6  1876  2sb5rf  1881  2sb6rf  1882  moabs  1965  moanim  1990  2eu4  2009  2eu7  2010  sb8ab  2175  risset  2369  reuind  2767  difundi  3217  indifdir  3221  unab  3232  inab  3233  rabeq0  3275  abeq0  3276  inssdif0im  3319  snprc  3463  snss  3522  unipr  3622  uni0b  3633  pwtr  3983  opm  3999  onintexmid  4325  elxp2  4391  opthprc  4419  xpiundir  4427  elvvv  4431  relun  4482  inopab  4496  difopab  4497  ralxpf  4510  rexxpf  4511  dmiun  4572  rniun  4762  cnvresima  4838  imaco  4854  fnopabg  5050  dff1o2  5159  idref  5424  imaiun  5427  opabex3d  5776  opabex3  5777  elixx3g  8871  elfz2  8983  elfzuzb  8986  divalgb  10237  alsconv  10506
 Copyright terms: Public domain W3C validator