NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  3bitri GIF version

Theorem 3bitri 262
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 240 . 2 (ψθ)
51, 4bitri 240 1 (φθ)
Colors of variables: wff setvar class
Syntax hints:  wb 176
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177
This theorem is referenced by:  bibi1i  305  orbi1i  506  orass  510  or32  513  pm5.32  617  an32  773  excxor  1309  trunanfal  1355  falxortru  1360  nic-axALT  1439  tbw-bijust  1463  rb-bijust  1514  19.43  1605  19.43OLD  1606  excom13  1743  nf4  1868  19.12vv  1898  3exdistr  1910  4exdistr  1911  eeeanv  1914  ee4anv  1915  sb3an  2070  sbnf2  2108  sb8eu  2222  2eu4  2287  2eu7  2290  2eu8  2291  r19.26-3  2748  rexcom13  2773  cbvreu  2833  ceqsex2  2895  ceqsex4v  2898  ralrab2  3002  rexrab2  3004  reu2  3024  rmo4  3029  reu8  3032  2reu5lem3  3043  rmo2  3131  rmo3  3133  eldif  3221  ss2rab  3342  rabss  3343  ssrab  3344  dfss4  3489  undi  3502  undif3  3515  difin2  3516  dfnul2  3552  disj4  3599  elimif  3691  disjsn  3786  ssunpr  3868  sspr  3869  sstp  3870  uni0b  3916  uni0c  3917  ssint  3942  iunss  4007  iundif2  4033  nincompl  4072  elpw12  4145  elpw11c  4147  eluni1g  4172  eqrelk  4212  opkelcokg  4261  opkelimagekg  4271  imacok  4282  sikexlem  4295  dfimak2  4298  dfpw12  4301  dfint3  4318  unipw1  4325  dfpw2  4327  sb8iota  4346  dfaddc2  4381  addcid1  4405  nnsucelrlem2  4425  nndisjeq  4429  ltfinex  4464  ssfin  4470  eqpwrelk  4478  ncfinraiselem2  4480  ncfinlowerlem1  4482  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  nnadjoinpw  4521  nnpweqlem1  4522  nnpweq  4523  srelk  4524  sfintfinlem1  4531  tfinnnlem1  4533  tfinnn  4534  spfinex  4537  vfinspsslem1  4550  dfop2lem1  4573  proj1op  4600  eqvinop  4606  opeq  4619  opeqexb  4620  brabsb  4698  opelopabf  4711  opabn0  4716  br1stg  4730  setconslem1  4731  setconslem2  4732  setconslem3  4733  setconslem6  4736  dfswap2  4741  dfid3  4768  xpiundi  4817  opeliunxp  4820  ssopr  4846  cnvuni  4895  elrn  4896  dmuni  4914  dmopab3  4917  elima1c  4947  elimapw11c  4948  brres  4949  elsnres  4996  intirr  5029  rnuni  5038  xpeq0  5046  ssrnres  5059  dminxp  5061  dmsnopg  5066  cnvresima  5077  imaco  5086  rnco  5087  coi1  5094  elxp4  5108  dffun2  5119  fun11  5159  fnres  5199  f1funfun  5263  dff1o2  5291  dff1o4  5294  eqfnfv3  5394  fnressn  5438  dff13  5471  dff1o6  5475  cnvswap  5510  cnvsi  5518  oprabid  5550  brco1st  5777  brco2nd  5778  trtxp  5781  elfix  5787  brimage  5793  oqelins4  5794  otsnelsi3  5805  releqmpt2  5809  composeex  5820  addcfnex  5824  funsex  5828  brpprod  5839  dmpprod  5840  crossex  5850  pw1fnf1o  5855  fvfullfunlem1  5861  transex  5910  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  eqerlem  5960  fundmen  6043  xpassenlem  6056  xpassen  6057  enpw1lem1  6061  enmap2lem1  6063  enmap1lem1  6069  enpw1pw  6075  enprmaplem1  6076  lecex  6115  ovmuc  6130  mucex  6133  ovcelem1  6171  ceex  6174  ce0nn  6180  el2c  6191  dflec3  6221  taddc  6229  tcfnex  6244  addccan2nclem1  6263  addccan2nclem2  6264  nmembers1lem1  6268  nncdiv3lem1  6275  nncdiv3lem2  6276  nnc3n3p1  6278  spacvallem1  6281  nchoicelem10  6298  nchoicelem11  6299  nchoicelem16  6304
  Copyright terms: Public domain W3C validator