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

Theorem 3bitri 204
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3bitri.1 (𝜑𝜓)
3bitri.2 (𝜓𝜒)
3bitri.3 (𝜒𝜃)
Assertion
Ref Expression
3bitri (𝜑𝜃)

Proof of Theorem 3bitri
StepHypRef Expression
1 3bitri.1 . 2 (𝜑𝜓)
2 3bitri.2 . . 3 (𝜓𝜒)
3 3bitri.3 . . 3 (𝜒𝜃)
42, 3bitri 182 . 2 (𝜓𝜃)
51, 4bitri 182 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:  bibi1i  226  an32  527  orbi1i  713  orass  717  or32  720  dcan  876  dn1dc  902  an6  1253  excxor  1310  trubifal  1348  truxortru  1351  truxorfal  1352  falxortru  1353  falxorfal  1354  alrot4  1416  excom13  1620  sborv  1813  3exdistr  1835  4exdistr  1836  eeeanv  1851  ee4anv  1852  ee8anv  1853  sb3an  1875  elsb3  1895  elsb4  1896  sb9  1898  sbnf2  1900  sbco4  1926  2exsb  1928  sb8eu  1956  sb8euh  1966  sbmo  2002  2eu4  2036  2eu7  2037  r19.26-3  2492  rexcom13  2524  cbvreu  2580  ceqsex2  2648  ceqsex4v  2651  spc3gv  2699  ralrab2  2767  rexrab2  2769  reu2  2790  rmo4  2795  reu8  2798  sbc3an  2885  rmo3  2915  dfss2  2998  ss2rab  3080  rabss  3081  ssrab  3082  dfdif3  3093  undi  3229  undif3ss  3242  difin2  3243  dfnul2  3270  disj  3309  disjsn  3473  uni0c  3648  ssint  3673  iunss  3740  ssextss  4004  eqvinop  4027  opcom  4034  opeqsn  4036  opeqpr  4037  brabsb  4045  opelopabf  4058  opabm  4064  pofun  4096  sotritrieq  4109  uniuni  4230  ordsucim  4273  opeliunxp  4442  xpiundi  4445  brinxp2  4454  ssrel  4475  reliun  4507  cnvuni  4570  dmopab3  4597  opelres  4666  elres  4695  elsnres  4696  intirr  4762  ssrnres  4814  dminxp  4816  dfrel4v  4823  dmsnm  4837  rnco  4878  sb8iota  4925  dffun2  4963  dffun4f  4969  funco  4991  funcnveq  5014  fun11  5018  isarep1  5037  dff1o4  5186  dff1o6  5468  oprabid  5589  mpt22eqb  5662  ralrnmpt2  5667  rexrnmpt2  5668  opabex3d  5800  opabex3  5801  xporderlem  5904  f1od2  5908  tfr0dm  5992  tfrexlem  6004  frec0g  6067  nnaord  6170  ecid  6257  xpsnen  6387  xpcomco  6392  xpassen  6396  nqnq0  6729  opelreal  7094  pitoregt0  7115  elnn0  8393  elxnn0  8456  elxr  8964  xrnepnf  8966  elfzuzb  9151  4fvwrd4  9263  elfzo2  9273  resqrexlemsqa  10095  isprm2  10690  isprm4  10692
  Copyright terms: Public domain W3C validator