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  878  dn1dc  904  an6  1255  excxor  1312  trubifal  1350  truxortru  1353  truxorfal  1354  falxortru  1355  falxorfal  1356  alrot4  1418  excom13  1622  sborv  1815  3exdistr  1837  4exdistr  1838  eeeanv  1853  ee4anv  1854  ee8anv  1855  sb3an  1877  elsb3  1897  elsb4  1898  sb9  1900  sbnf2  1902  sbco4  1928  2exsb  1930  sb8eu  1958  sb8euh  1968  sbmo  2004  2eu4  2038  2eu7  2039  r19.26-3  2495  rexcom13  2528  cbvreu  2584  ceqsex2  2653  ceqsex4v  2656  spc3gv  2704  ralrab2  2771  rexrab2  2773  reu2  2794  rmo4  2799  reu8  2802  sbc3an  2889  rmo3  2919  dfss2  3003  ss2rab  3086  rabss  3087  ssrab  3088  dfdif3  3099  undi  3236  undif3ss  3249  difin2  3250  dfnul2  3277  disj  3319  disjsn  3489  uni0c  3664  ssint  3689  iunss  3756  ssextss  4023  eqvinop  4046  opcom  4053  opeqsn  4055  opeqpr  4056  brabsb  4064  opelopabf  4077  opabm  4083  pofun  4115  sotritrieq  4128  uniuni  4249  ordsucim  4292  opeliunxp  4463  xpiundi  4466  brinxp2  4475  ssrel  4496  reliun  4528  cnvuni  4592  dmopab3  4619  opelres  4688  elres  4717  elsnres  4718  intirr  4787  ssrnres  4841  dminxp  4843  dfrel4v  4850  dmsnm  4864  rnco  4905  sb8iota  4955  dffun2  4993  dffun4f  4999  funco  5021  funcnveq  5044  fun11  5048  isarep1  5067  dff1o4  5226  dff1o6  5518  oprabid  5640  mpt22eqb  5713  ralrnmpt2  5718  rexrnmpt2  5719  opabex3d  5851  opabex3  5852  xporderlem  5955  f1od2  5959  tfr0dm  6043  tfrexlem  6055  frec0g  6118  nnaord  6222  ecid  6309  mapsnen  6482  xpsnen  6491  xpcomco  6496  xpassen  6500  nqnq0  6947  opelreal  7312  pitoregt0  7333  elnn0  8611  elxnn0  8674  elxr  9182  xrnepnf  9184  elfzuzb  9369  4fvwrd4  9482  elfzo2  9492  resqrexlemsqa  10374  isprm2  11024  isprm4  11026
  Copyright terms: Public domain W3C validator