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

Theorem 3bitri 195
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 173 . 2 (ψθ)
51, 4bitri 173 1 (φθ)
Colors of variables: wff set class
Syntax hints:  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  bibi1i  217  an32  484  orbi1i  667  orass  671  or32  674  dcan  830  dn1dc  855  an6  1201  excxor  1254  trubifal  1290  truxortru  1293  truxorfal  1294  falxortru  1295  falxorfal  1296  alrot4  1355  alrot4OLD  1356  excom13  1561  sborv  1752  3exdistr  1774  4exdistr  1775  eeeanv  1790  ee4anv  1791  ee8anv  1792  sb3an  1814  elsb3  1834  elsb4  1835  sb9  1837  sbnf2  1839  sbco4  1865  2exsb  1867  sb8eu  1895  sb8euh  1905  sbmo  1941  2eu4  1975  2eu7  1976  r19.26-3  2421  rexcom13  2453  cbvreu  2509  ceqsex2  2571  ceqsex4v  2574  spc3gv  2622  ralrab2  2683  rexrab2  2685  reu2  2706  rmo4  2711  reu8  2714  rmo3  2826  dfss2  2911  ss2rab  2993  rabss  2994  ssrab  2995  undi  3162  undif3ss  3175  difin2  3176  dfnul2  3203  disj  3245  disjsn  3406  uni0c  3580  ssint  3605  iunss  3672  ssextss  3930  eqvinop  3954  opcom  3961  opeqsn  3963  opeqpr  3964  brabsb  3972  opelopabf  3985  opabm  3991  pofun  4023  sotritrieq  4036  uniuni  4133  ordsucim  4176  opeliunxp  4322  xpiundi  4325  brinxp2  4334  ssrel  4355  reliun  4385  cnvuni  4448  dmopab3  4475  opelres  4544  elres  4573  elsnres  4574  intirr  4638  ssrnres  4690  dminxp  4692  dfrel4v  4699  dmsnm  4713  rnco  4754  sb8iota  4801  dffun2  4839  dffun4f  4844  funco  4866  funcnveq  4888  fun11  4892  isarep1  4911  dff1o4  5059  dff1o6  5341  oprabid  5461  mpt22eqb  5533  ralrnmpt2  5538  rexrnmpt2  5539  opabex3d  5671  opabex3  5672  xporderlem  5774  tfrexlem  5870  frec0g  5902  nnaord  5993  ecid  6080  nqnq0  6296  opelreal  6540
  Copyright terms: Public domain W3C validator