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

Theorem bitri 183
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 119 . . 3 (𝜑𝜓)
3 bitri.2 . . 3 (𝜓𝜒)
42, 3sylib 121 . 2 (𝜑𝜒)
53biimpri 132 . . 3 (𝜒𝜓)
65, 1sylibr 133 . 2 (𝜒𝜑)
74, 6impbii 125 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  bitr2i  184  bitr3i  185  bitr4i  186  bitrd  187  3bitri  205  3bitr2i  207  3bitr3i  209  3bitr4i  211  bibi12i  228  imbi12i  238  pm4.71r  388  biadan2  452  anbi2ci  455  anbi12i  456  anbi12ci  457  pm5.3  467  an42  577  xchbinx  672  mt2bi  674  orbi12i  754  or42  762  pm5.53  792  orddi  810  anddi  811  pm2.1dc  823  dcim  827  notnotrdc  829  dcnnOLD  835  rbaib  907  rbaibr  908  pm4.43  934  orbididc  938  pm5.75  947  3orass  966  3anass  967  3ancomb  971  3anan32  974  3anan12  975  anandi3  976  anandi3r  977  xordc  1371  falbitru  1396  19.26-2  1459  19.26-3an  1460  alrot3  1462  albiim  1464  2albiim  1465  19.27h  1540  19.27  1541  19.28h  1542  19.28  1543  nfalt  1558  aaanh  1566  aaan  1567  alinexa  1583  19.21-2  1646  nf2  1647  19.44  1661  19.45  1662  exrot3  1669  exrot4  1670  eeor  1674  sbcof2  1783  sbid2h  1822  19.23vv  1857  sbnv  1861  sblimv  1867  pm11.53  1868  19.41vv  1876  19.41vvv  1877  19.41vvvv  1878  exdistrv  1883  19.42vv  1884  19.42vvv  1885  19.42vvvv  1886  4exdistr  1889  cbvex4v  1903  eean  1904  sbn  1926  sbim  1927  sbor  1928  sban  1929  sbrim  1930  sblim  1931  sbbi  1933  sblbis  1934  sbrbis  1935  sbrbif  1936  sbco2d  1940  sbco2vd  1941  sbnf2  1957  2sb5  1959  2sb6  1960  sbcom2v  1961  sbcom2v2  1962  sbcom2  1963  sb6a  1964  2sb5rf  1965  2sb6rf  1966  sbalyz  1975  sbal  1976  sbal1yz  1977  sbex  1980  sbalv  1981  sbco4lem  1982  exsb  1984  2exsb  1985  eujust  2002  euf  2005  cbveu  2024  mor  2042  eu2  2044  mo4f  2060  eu4  2062  2exeu  2092  2eu4  2093  exists1  2096  abid  2128  eleq12i  2208  abeq2  2249  abeq2i  2251  clabel  2267  abid2f  2307  sbabel  2308  neeq12i  2326  neanior  2396  ralnex  2427  dfrex2dc  2429  ralinexa  2465  nfraldya  2472  nfrexdya  2473  r3al  2480  r19.26-2  2564  ralbiim  2569  ralnex2  2574  r19.43  2592  ralcomf  2595  rexcomf  2596  rexrot4  2600  reean  2602  3reeanv  2604  rabbi  2611  cbvralf  2651  cbvrexf  2652  cbvreu  2655  cbvral2v  2668  cbvrex2v  2669  cbvral3v  2670  cbvralsv  2671  cbvrexsv  2672  sbralie  2673  rabeq2i  2686  issetf  2696  2gencl  2722  3gencl  2723  ceqsex2  2729  ceqsex3v  2731  ceqsex6v  2733  ceqsex8v  2734  gencbvex  2735  gencbval  2737  spc2gv  2779  eqvincf  2813  ceqsrex2v  2820  elrab2  2846  ralab  2847  ralrab  2848  rexab  2849  rexrab  2850  ralab2  2851  rexab2  2853  eueq3dc  2861  morex  2871  euind  2874  reu2  2875  reu6  2876  rmo4  2880  reu4  2881  reu7  2882  rmo3f  2884  rmo4f  2885  rmoim  2888  2reuswapdc  2891  reuind  2892  2rmorex  2893  sbcco  2933  sbccomlem  2986  sbccom  2987  ra5  3000  rmo3  3003  csbco  3016  sbnfc2  3063  csbabg  3064  cbvralcsf  3065  cbvrexcsf  3066  cbvreucsf  3067  dfss  3088  dfss2f  3091  ss2ab  3168  dfdif3  3189  difeqri  3199  ddifstab  3211  raldifb  3219  uneqri  3221  ssequn2  3252  unss  3253  rexun  3259  ralunb  3260  elin2  3267  ineqri  3272  dfss1  3283  dfss5  3284  dfss4st  3312  ssddif  3313  difin  3316  indif  3322  difundi  3331  indifdir  3335  symdifxor  3345  inrab2  3352  rabun2  3358  reuun2  3362  0el  3388  rabeq0  3395  abeq0  3396  disjr  3415  disj1  3416  undif4  3428  uneqdifeqim  3451  r19.2m  3452  r19.3rm  3454  r19.9rmv  3457  raaan  3472  pwss  3529  dfpr2  3549  rexdifpr  3558  ralsnsg  3566  ralsns  3567  eltpg  3574  eldiftp  3575  ralprg  3580  rexprg  3581  raltpg  3582  rextpg  3583  snprc  3594  rabrsndc  3597  euabsn2  3598  eusn  3603  eldifsn  3656  ssdifsn  3657  rexdifsn  3661  eqsnm  3688  tpss  3691  snsssn  3694  prel12  3704  preqsn  3708  oprcl  3735  pwtpss  3739  eluniab  3754  elunirab  3755  unipr  3756  dfnfc2  3760  uniun  3761  uniin  3762  uni0b  3767  unissb  3772  elintab  3788  elintrab  3789  ssintab  3794  ssintrab  3800  intun  3808  intpr  3809  elrint  3817  iuncom4  3826  iuneq2  3835  dfiun2g  3851  ssiinf  3868  iundif2ss  3884  elriin  3889  iunxiun  3900  pwssb  3904  elpwpw  3905  iunpwss  3910  dfdisj2  3914  disjiun  3930  cbvopab1  4007  dftr5  4035  trint  4047  inex1  4068  inuni  4086  repizf2lem  4091  unidif0  4097  axpweq  4101  bnd2  4103  exmid01  4127  zfpair2  4138  exss  4155  elop  4159  opm  4162  otth  4170  copsex4g  4175  opeqsn  4180  opelopabsbALT  4187  brabga  4192  opelopabaf  4201  iunopab  4209  pwunss  4211  pocl  4231  frirrg  4278  elsuci  4331  elsucg  4332  sucel  4338  unisucg  4342  uniuni  4378  reusv3  4387  iunpw  4407  setindel  4459  elirr  4462  en2lp  4475  ordpwsucss  4488  zfregfr  4494  tfi  4502  peano2  4515  peano5  4518  elxp  4562  opelxp  4575  brxp  4576  rabxp  4582  opthprc  4596  brab2a  4598  opeliunxp  4600  xpundi  4601  xpundir  4602  elvvv  4608  brinxp  4613  brab2ga  4620  0xp  4625  ssrel2  4635  eqrelrel  4646  reliun  4666  reluni  4668  raliunxp  4686  rexiunxp  4687  ralxpf  4691  rexxpf  4692  iunxpf  4693  relop  4695  elco  4711  elcnv  4722  elcnv2  4723  dmin  4753  dmuni  4755  dmopab  4756  dmi  4760  dmmrnm  4764  rnopab  4792  elrnmpt1  4796  rncoeq  4818  resiexg  4870  dfima2  4889  dfima3  4890  elima2  4893  elima3  4894  imai  4901  elimasn  4912  epini  4916  dfse2  4918  cotr  4926  issref  4927  intasym  4929  asymref  4930  cnvopab  4946  cnvi  4949  cnvdif  4951  imainss  4960  rnxpid  4979  dfrel2  4995  dfrel3  5002  dmsnm  5010  rnsnm  5011  relsn2m  5015  dmsnopg  5016  cnvcnvsn  5021  elxp4  5032  elxp5  5033  cnvresima  5034  mptpreima  5038  dfco2  5044  coundi  5046  coundir  5047  imaco  5050  coiun  5054  coi1  5060  relssdmrn  5065  relrelss  5071  unixpm  5080  ressn  5085  cnviinm  5086  cnvpom  5087  cnvsom  5088  cbviota  5099  iotass  5111  dffun2  5139  dffun4  5140  dffun7  5156  dffun8  5157  dffun9  5158  funopab  5164  funun  5173  funcnvsn  5174  fntpg  5185  funcnv2  5189  funcnv  5190  fun2cnv  5193  fncnv  5195  fun11  5196  fununi  5197  imadiflem  5208  imadif  5209  imainlem  5210  funimaexglem  5212  fnunsn  5236  fnres  5245  fnopabg  5252  mptfng  5254  mptun  5260  fun  5301  fcnvres  5312  dff12  5333  f1cnvcnv  5345  funforn  5358  dff1o2  5378  dff1o5  5382  f1orn  5383  resdif  5395  ffoss  5405  f11o  5406  f1o00  5408  fo00  5409  elfv  5425  fv3  5450  nfvres  5460  eqfnfv3  5526  fneqeql  5534  unpreima  5551  respreima  5554  dffo3  5573  dffo5  5575  f1ompt  5577  ffnfvf  5585  fmptco  5592  ftpg  5610  fnressn  5612  idref  5664  abrexco  5666  dff13  5675  dff13f  5677  fliftel  5700  isoini  5725  eusvobj2  5766  acexmidlema  5771  acexmidlemb  5772  acexmidlemph  5773  acexmidlem2  5777  oprabid  5809  brabvv  5823  dfoprab2  5824  eqoprab2b  5835  dmoprab  5858  rnoprab  5860  eloprabga  5864  mpomptx  5868  resoprab  5873  ffnov  5881  elrnmpo  5890  ralrnmpo  5891  rexrnmpo  5892  ovid  5893  ovi3  5913  ov6g  5914  foov  5923  opabex3d  6025  opabex3  6026  abexssex  6029  oprabex3  6033  oprabrexex2  6034  fmpo  6105  xporderlem  6134  f1od2  6138  mpoxopovel  6144  brtpos2  6154  dmtpos  6159  tpostpos  6167  tpossym  6179  tposoprab  6183  dfsmo2  6190  tfrlem7  6220  tfrlem9  6222  tfr1onlemaccex  6251  tfrcllemaccex  6264  tfrcldm  6266  frecabex  6301  el1o  6340  dif1o  6341  dfer2  6436  brdifun  6462  eqerlem  6466  qsid  6500  iinerm  6507  riinerm  6508  erinxp  6509  brecop  6525  eroveu  6526  erovlem  6527  ecopovsym  6531  mapval2  6578  mapsn  6590  elixp  6605  ixpeq2  6612  ixpin  6623  ixpiinm  6624  mptelixpg  6634  ixpsnf1o  6636  domen  6651  isfi  6661  en1  6699  xpsnen  6721  xpcomco  6726  xpassen  6730  ssenen  6751  nneneq  6757  snnen2oprc  6760  ac6sfi  6798  exmidpw  6808  eldju  6959  djur  6960  eldju2ndl  6963  eldju2ndr  6964  finomni  7018  acfun  7078  ccfunen  7094  elni  7138  ltexpi  7167  enq0enq  7261  enq0ref  7263  enq0tr  7264  prarloclem3  7327  ltdfpr  7336  genpdflem  7337  genpassl  7354  genpassu  7355  nqprrnd  7373  nqprl  7381  nqpru  7382  ltexprlemopl  7431  ltexprlemopu  7433  ltexprlemdisj  7436  ltexprlemloc  7437  recexprlemdisj  7460  caucvgprprlemell  7515  caucvgprprlemelu  7516  suplocexprlemml  7546  suplocsrlemb  7636  opelcn  7656  elreal  7658  elreal2  7660  peano1nnnn  7682  axicn  7693  axaddf  7698  axmulf  7699  axprecex  7710  axpre-ltirr  7712  axpre-mulgt0  7717  axcaucvglemres  7729  axpre-suploc  7732  xrlenlt  7851  ltxrlt  7852  inelr  8368  reapcotr  8382  1nn  8753  elnnne0  9013  un0addcl  9032  un0mulcl  9033  elnnz  9086  elznn0nn  9090  elznn0  9091  elznn  9092  elz2  9144  zapne  9147  3halfnz  9170  prime  9172  raluz2  9399  rexuz2  9401  supinfneg  9415  infsupneg  9416  eluz2b2  9422  eluz2b3  9423  ublbneg  9430  elq  9439  qreccl  9459  elpq  9465  ralrp  9490  rexrp  9491  rpnegap  9501  ltxr  9590  xrnemnf  9592  xrltso  9610  icc0r  9737  divelunit  9813  fzprval  9891  fztpval  9892  elfz1b  9899  fz01or  9920  4fvwrd4  9946  fzolb  9959  fzolb2  9960  elfzo3  9969  fzouzsplit  9985  elfzo0z  9990  fzo0m  9997  fzind2  10045  ioo0  10066  ico0  10068  ioc0  10069  uzennn  10238  seq3f1olemp  10304  caucvgre  10783  cvg1nlemcau  10786  resqrexlemex  10827  climeu  11095  fsum2dlemstep  11233  expcnv  11303  divides  11524  m1exp1  11627  divalgb  11651  bezoutlemnewy  11713  bezoutlemmain  11715  bezoutlemex  11718  dfgcd2  11731  lcmgcdlem  11787  isprm2  11827  isprm3  11828  isprm4  11829  sqrt2irr  11869  oddpwdc  11881  ennnfoneleminc  11953  ennnfonelemex  11956  ennnfonelemr  11965  ctiunct  11982  istps  12231  istps2  12232  isbasis2g  12244  tgval2  12252  txuni2  12457  tx1cn  12470  tx2cn  12471  uptx  12475  txdis1cn  12479  blres  12635  xmeterval  12636  xmeter  12637  isxms2  12653  isms2  12655  metrest  12707  qtopbasss  12722  dedekindicclemicc  12811  limcdifap  12832  pilem1  12901  sincosq1lem  12947  decidr  13167  bdcuni  13238  bdcriota  13245  bdinex1  13261  bj-zfpair2  13272  bj-axun2  13277  bj-ssom  13298  ss1oel2o  13353  nninfsellemdc  13374  nninfsellemsuc  13376  nninfsellemqall  13379  trirec0xor  13406
  Copyright terms: Public domain W3C validator