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

Theorem bitri 240
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.)
Hypotheses
Ref Expression
bitri.1 (φψ)
bitri.2 (ψχ)
Assertion
Ref Expression
bitri (φχ)

Proof of Theorem bitri
StepHypRef Expression
1 bitri.1 . . . 4 (φψ)
21biimpi 186 . . 3 (φψ)
3 bitri.2 . . 3 (ψχ)
42, 3sylib 188 . 2 (φχ)
53biimpri 197 . . 3 (χψ)
65, 1sylibr 203 . 2 (χφ)
74, 6impbii 180 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:  bitr2i  241  bitr3i  242  bitr4i  243  bitrd  244  3bitri  262  3bitr2i  264  3bitr3i  266  3bitr4i  268  xchbinx  301  bibi12i  306  imbi12i  316  mt2bi  328  iman  413  orbi12i  507  or42  515  pm4.71r  612  biadan2  623  anbi2ci  677  anbi12i  678  anbi12ci  679  pm5.3  692  pm5.53  771  an42  798  orddi  839  anddi  840  rbaib  873  rbaibr  874  pm4.43  893  biluk  899  pm5.75  903  dn1  932  3orass  937  3anass  938  3ancomb  943  3anan32  946  3anan12  947  3anor  948  an6  1261  xor2  1310  falbitru  1352  falnantru  1356  truxortru  1358  truxorfal  1359  falxorfal  1361  exp3acom23g  1371  hadass  1386  hadbi  1387  hadrot  1390  cador  1391  cadan  1392  cadnot  1394  cadcomb  1396  cadrot  1397  cad1  1398  had1  1402  alex  1572  alinexa  1578  alexn  1579  exanali  1585  19.26-2  1594  19.26-3an  1595  albiim  1611  2albiim  1612  ax12bOLD  1690  alrot3  1738  alrot4  1739  exrot3  1744  exrot4  1745  19.21-2  1864  nf2  1866  19.27  1869  19.28  1870  19.36  1871  19.37  1873  19.44  1877  19.45  1878  aaan  1884  eeor  1885  19.23vv  1892  pm11.53  1893  19.41vv  1902  19.41vvv  1903  19.41vvvv  1904  19.42vv  1907  19.42vvv  1908  4exdistr  1911  eean  1912  cbvex4v  2012  sbor  2066  sbrim  2067  sblim  2068  sban  2069  sbbi  2071  sblbis  2072  sbrbis  2073  sbrbif  2074  sbid2  2084  sbco2d  2087  sb8e  2093  sbnf2  2108  2sb5  2112  2sb6  2113  sbcom2  2114  sb6a  2116  2sb5rf  2117  2sb6rf  2118  sbex  2128  sbalv  2129  exsbOLD  2131  2exsb  2132  eujust  2206  euf  2210  cbveu  2224  eu2  2229  mo2  2233  sbmo  2234  mo3  2235  mo4f  2236  eu4  2243  moanim  2260  2mo  2282  2mos  2283  2eu1  2284  2eu3  2286  2eu4  2287  2eu6  2289  exists1  2293  abid  2341  eleq12i  2418  abeq2  2458  abeq2i  2460  clabel  2474  abid2f  2514  sbabel  2515  neeq12i  2528  necon1abii  2567  neanior  2601  ralnex  2624  rexnal  2625  ralinexa  2659  rexanali  2660  r3al  2671  r19.26-2  2747  ralbiim  2751  r19.30  2756  ralcomf  2769  rexcomf  2770  rexrot4  2774  reean  2777  3reeanv  2779  rabbi  2789  cbvralf  2829  cbvreu  2833  cbvral2v  2843  cbvrex2v  2844  cbvral3v  2845  cbvralsv  2846  cbvrexsv  2847  sbralie  2848  rabeq2i  2856  issetf  2864  2gencl  2888  3gencl  2889  ceqsex2  2895  ceqsex3v  2897  ceqsex6v  2899  ceqsex8v  2900  gencbvex  2901  spc3gv  2944  eqvincf  2967  ceqsrex2v  2974  elrab2  2996  ralab  2997  ralrab  2998  rexab  2999  rexrab  3000  ralab2  3001  rexab2  3003  eueq3  3011  morex  3020  euxfr2  3021  euxfr  3022  euind  3023  reu2  3024  reu6  3025  rmo4  3029  reu4  3030  reu7  3031  rmoim  3035  2reuswap  3038  reuind  3039  2reu5lem1  3041  2reu5lem2  3042  2reu5  3044  sbcco  3068  sbccomlem  3116  sbccom  3117  ra5  3130  rmo3  3133  csbco  3145  sbnfc2  3196  csbabg  3197  cbvralcsf  3198  cbvreucsf  3200  elsymdif  3223  dfss  3260  dfss2  3262  dfss2f  3264  ss2ab  3334  dfpss2  3354  dfpss3  3355  psseq12i  3360  sspsstri  3371  difeqri  3387  uneqri  3406  ssequn2  3436  unss  3437  rexun  3443  ralunb  3444  elin2  3446  ineqri  3449  dfss1  3460  dfss5  3461  nsspssun  3488  indifdir  3511  inrab2  3528  rabun2  3534  reuun2  3538  eq0  3564  0el  3566  abn0  3568  0pss  3588  disjr  3592  disj1  3593  disjpss  3601  undif4  3607  difin0ss  3616  inssdif0  3617  uneqdifeq  3638  r19.3rz  3641  r19.3rzv  3643  ralidm  3653  pwss  3736  dfpr2  3749  ralsns  3763  rexsns  3764  eltpg  3769  ralprg  3775  rexprg  3776  raltpg  3777  rextpg  3778  euabsn2  3791  eusn  3796  eldifsn  3839  rexdifsn  3843  difsnpss  3851  pwpw0  3855  ssunsn  3866  eqsn  3867  sstp  3870  tpss  3871  pwsnALT  3882  pwtp  3884  dfpss4  3888  eluniab  3903  elunirab  3904  unipr  3905  dfnfc2  3909  uniun  3910  uniin  3911  unissb  3921  elintab  3937  elintrab  3938  ssintab  3943  ssintrab  3949  intun  3958  intpr  3959  elrint  3967  iuncom4  3976  iuneq2  3985  dfiun2g  3999  ssiinf  4015  elriin  4038  iunxiun  4048  pwssb  4052  iunpwss  4055  ssofss  4076  axprimlem1  4088  axprimlem2  4089  axcnvprim  4091  axssetprim  4092  axsiprim  4093  axtyplowerprim  4094  axins2prim  4095  axins3prim  4096  ninexg  4097  snex  4111  pwadjoin  4119  elopk  4129  1cex  4142  elpw1  4144  snelpw1  4146  elpw11c  4147  elpw121c  4148  elpw131c  4149  elpw141c  4150  elpw151c  4151  elpw161c  4152  elpw171c  4153  elpw181c  4154  elpw191c  4155  elpw1101c  4156  elpw1111c  4157  0nel1c  4159  eqpw1  4162  pw1un  4163  pw111  4170  ssrelk  4211  eqrelk  4212  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  elp6  4263  opksnelsik  4265  opkelimagekg  4271  cnvkxpk  4276  inxpk  4277  elimaksn  4283  cokrelk  4284  xpkvexg  4285  cnvkexg  4286  p6exg  4290  ssetkex  4294  sikexlem  4295  sikexg  4296  dfimak2  4298  insklem  4304  ins2kexg  4305  ins3kexg  4306  dfidk2  4313  dfuni3  4315  dfint3  4318  ndisjrelk  4323  dfpw2  4327  cbviota  4344  dfiota4  4372  dfaddc2  4381  dfnnc2  4395  0nelsuc  4400  peano1  4402  peano2  4403  addccom  4406  peano5  4409  nnc0suc  4412  elsuc  4413  addcass  4415  elfin  4420  el0c  4421  nnsucelrlem1  4424  nnsucelrlem2  4425  nnsucelr  4428  nndisjeq  4429  preaddccan2lem1  4454  ltfinex  4464  ltfintrilem1  4465  ssfin  4470  eqpwrelk  4478  eqpw1relk  4479  ncfinraiselem2  4480  ncfinlowerlem1  4482  ncfinlower  4483  nnpw1ex  4484  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenoddnnnul  4514  evenodddisjlem1  4515  evenodddisj  4516  nnadjoinlem1  4519  nnadjoin  4520  nnpweqlem1  4522  nnpweq  4523  srelk  4524  sfintfinlem1  4531  tfinnnlem1  4533  tfinnn  4534  spfinex  4537  spfinsfincl  4539  vfinspsslem1  4550  vfinspss  4551  vfinspclt  4552  vfinncsp  4554  dfphi2  4569  dfop2lem1  4573  dfop2lem2  4574  dfop2  4575  dfproj22  4577  phi011lem1  4598  phi011  4599  proj2op  4601  eqvinop  4606  copsex4g  4610  eqop  4611  phidisjnn  4615  phialllem1  4616  phiall  4618  cbvopab1  4632  brabga  4701  opelopabaf  4710  opabn0  4716  el1st  4729  br1stg  4730  setconslem1  4731  setconslem2  4732  setconslem3  4733  setconslem4  4734  setconslem6  4736  setconslem7  4737  df1st2  4738  elswap  4740  dfswap2  4741  dfima2  4745  dfco1  4748  dfsi2  4751  elima2  4755  elima3  4756  dfid3  4768  elxp  4801  opelxp  4811  brxp  4812  rabxp  4814  opeliunxp  4820  eliunxp  4821  raliunxp  4823  rexiunxp  4824  ralxpf  4827  rexxpf  4828  iunxpf  4829  xpundi  4832  xpundir  4833  brinxp2  4835  brinxp  4836  xp0r  4842  ssopr  4846  eqopr  4847  brswap2  4860  elcnv  4889  elcnv2  4890  cnvco  4894  elrn2  4897  eldm  4898  eldm2  4899  dmun  4912  dmin  4913  dmuni  4914  dmopab  4915  dmi  4919  elimapw1  4944  elimapw12  4945  elimapw13  4946  elimapw11c  4948  dfima3  4951  dfima4  4952  rnopab  4967  rneq0  4970  dmcoss  4971  dmcosseq  4973  rncoeq  4975  dmres  4986  resabs1  4992  elres  4995  dfres2  5002  imai  5010  epini  5021  cotr  5026  intasym  5028  intirr  5029  cnvopab  5030  cnvi  5032  imainss  5042  cnvcnv  5062  dmsnn0  5064  rnsnn0  5065  dmsnopg  5066  cnvsn  5073  rnsnop  5075  cnvresima  5077  dfco2  5080  dfco2a  5081  coundi  5082  coundir  5083  coiun  5090  co01  5093  coi1  5094  dfcnv2  5100  elxp4  5108  df2nd2  5111  dfxp2  5113  cnviin  5118  dffun2  5119  dffun3  5120  dffun4  5121  dffun5  5122  dffun8  5134  dffun9  5135  nfunv  5138  funopab  5139  funun  5146  funsn  5147  funcnv2  5155  funcnv  5156  fncnv  5158  fun11  5159  fununi  5160  imadif  5171  fnunsn  5190  fnres  5199  iunfopab  5204  fnopabg  5205  fnopab2g  5206  fun  5236  fcnvres  5243  dff12  5257  funforn  5276  dff1o2  5291  dff1o3  5292  dff1o5  5295  f1ocnvb  5298  resdif  5306  f1ococnv2  5309  ffoss  5314  f11o  5315  f1o00  5317  fo00  5318  elfv  5326  fv3  5341  nfvres  5352  fnrnfv  5364  dmfco  5381  eqfnfv3  5394  unpreima  5408  respreima  5410  fnasrn  5417  dff4  5421  dffo3  5422  dffo5  5424  ffnfvf  5428  fopabfv  5430  fsn2  5434  fconst3  5457  fconst4  5458  funfvima  5459  abrexco  5463  funiunfv  5467  dff13  5471  dff13f  5472  isocnv2  5492  isomin  5496  isoini  5497  opbr1st  5501  opbr2nd  5502  dfid4  5503  swapf1o  5511  xpnedisj  5513  dmsi  5519  oprabid  5550  dfoprab2  5558  dmoprab  5574  rnoprab  5576  eloprabga  5578  resoprab  5581  ffnov  5587  fnov  5591  fov  5592  ovidig  5593  ov3  5599  ov6g  5600  foov  5606  ndmovcl  5614  ndmov  5615  ndmovdistr  5619  mptpreima  5682  mpt2mptx  5708  fmpt2  5731  brsnsi  5773  brsnsi1  5775  brsnsi2  5776  brco1st  5777  brco2nd  5778  trtxp  5781  brtxp  5783  restxp  5786  elfix  5787  otelins2  5791  otelins3  5792  brimage  5793  oqelins4  5794  dmtxp  5802  txpcofun  5803  otsnelsi3  5805  releqel  5807  releqmpt  5808  releqmpt2  5809  cupex  5816  composeex  5820  disjex  5823  addcfnex  5824  epprc  5827  funsex  5828  fnsex  5832  qrpprod  5836  brpprod  5839  dmpprod  5840  fnpprod  5843  brcrossg  5848  crossex  5850  pw1fnex  5852  pw1fnf1o  5855  fnfullfunlem1  5856  fvfullfunlem3  5863  domfnex  5870  ranfnex  5871  clos1ex  5876  clos1conn  5879  clos1induct  5880  clos1is  5881  dfnnc3  5885  transex  5910  refex  5911  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  ersymtr  5932  porta  5933  sopc  5934  frds  5935  weds  5938  eqerlem  5960  qsexg  5982  qsid  5990  mapexi  6003  pmvalg  6010  mapval2  6018  enex  6031  xpassenlem  6056  xpassen  6057  enpw1lem1  6061  enmap2lem1  6063  enmap2lem4  6066  enmap1lem1  6069  enmap1lem4  6072  enpw1pw  6075  enprmaplem1  6076  enprmaplem4  6079  nenpw1pwlem1  6084  brltc  6114  lecex  6115  elncs  6119  elnc  6125  ovmuc  6130  mucex  6133  1cnc  6139  peano4nc  6150  ncssfin  6151  ncspw1eu  6159  ovcelem1  6171  ceexlem1  6173  ceex  6174  fnce  6176  ce0nnul  6177  ce0nn  6180  fce  6188  el2c  6191  lec0cg  6198  sbthlem1  6203  sbth  6206  addlec  6208  nc0le1  6216  leconnnc  6218  dflec3  6221  nclenc  6222  lenc  6223  tc11  6228  taddc  6229  letc  6231  tcfnex  6244  nclennlem1  6248  muc0or  6252  csucex  6259  nnltp1clem1  6261  addccan2nclem1  6263  addccan2nclem2  6264  nmembers1lem1  6268  nmembers1lem2  6269  nmembers1lem3  6270  ltcirr  6272  nncdiv3lem1  6275  nncdiv3lem2  6276  nncdiv3  6277  nnc3n3p1  6278  nnc3n3p2  6279  spacvallem1  6281  spacind  6287  spacis  6288  nchoicelem6  6294  nchoicelem8  6296  nchoicelem9  6297  nchoicelem10  6298  nchoicelem11  6299  nchoicelem12  6300  nchoicelem14  6302  nchoicelem16  6304  nchoicelem18  6306  nchoicelem19  6307  dmfrec  6316  fnfreclem1  6317  scancan  6331
  Copyright terms: Public domain W3C validator