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

Theorem 3bitri 199
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 177 . 2 (𝜓𝜃)
51, 4bitri 177 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:  bibi1i  221  an32  504  orbi1i  690  orass  694  or32  697  dcan  853  dn1dc  878  an6  1227  excxor  1285  trubifal  1323  truxortru  1326  truxorfal  1327  falxortru  1328  falxorfal  1329  alrot4  1391  excom13  1595  sborv  1786  3exdistr  1808  4exdistr  1809  eeeanv  1824  ee4anv  1825  ee8anv  1826  sb3an  1848  elsb3  1868  elsb4  1869  sb9  1871  sbnf2  1873  sbco4  1899  2exsb  1901  sb8eu  1929  sb8euh  1939  sbmo  1975  2eu4  2009  2eu7  2010  r19.26-3  2460  rexcom13  2492  cbvreu  2548  ceqsex2  2611  ceqsex4v  2614  spc3gv  2662  ralrab2  2728  rexrab2  2730  reu2  2751  rmo4  2756  reu8  2759  sbc3an  2846  rmo3  2876  dfss2  2961  ss2rab  3043  rabss  3044  ssrab  3045  undi  3212  undif3ss  3225  difin2  3226  dfnul2  3253  disj  3295  disjsn  3459  uni0c  3633  ssint  3658  iunss  3725  ssextss  3983  eqvinop  4007  opcom  4014  opeqsn  4016  opeqpr  4017  brabsb  4025  opelopabf  4038  opabm  4044  pofun  4076  sotritrieq  4089  uniuni  4210  ordsucim  4253  opeliunxp  4422  xpiundi  4425  brinxp2  4434  ssrel  4455  reliun  4485  cnvuni  4548  dmopab3  4575  opelres  4644  elres  4673  elsnres  4674  intirr  4738  ssrnres  4790  dminxp  4792  dfrel4v  4799  dmsnm  4813  rnco  4854  sb8iota  4901  dffun2  4939  dffun4f  4945  funco  4967  funcnveq  4989  fun11  4993  isarep1  5012  dff1o4  5161  dff1o6  5443  oprabid  5564  mpt22eqb  5637  ralrnmpt2  5642  rexrnmpt2  5643  opabex3d  5775  opabex3  5776  xporderlem  5879  f1od2  5883  tfr0  5967  tfrexlem  5978  frec0g  6013  nnaord  6112  ecid  6199  xpsnen  6325  xpcomco  6330  xpassen  6334  nqnq0  6596  opelreal  6961  pitoregt0  6982  elnn0  8240  elxr  8796  xrnepnf  8800  elfzuzb  8985  4fvwrd4  9098  elfzo2  9108  resqrexlemsqa  9843
  Copyright terms: Public domain W3C validator