Theorem bitri 182

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

Step	Hyp	Ref	Expression
1		bitri.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 118	. . 3 ⊢ (𝜑 → 𝜓)
3		bitri.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
4	2, 3	sylib 120	. 2 ⊢ (𝜑 → 𝜒)
5	3	biimpri 131	. . 3 ⊢ (𝜒 → 𝜓)
6	5, 1	sylibr 132	. 2 ⊢ (𝜒 → 𝜑)
7	4, 6	impbii 124	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bitr2i  183  bitr3i  184  bitr4i  185  bitrd  186  3bitri  204  3bitr2i  206  3bitr3i  208  3bitr4i  210  bibi12i  227  imbi12i  237  pm4.71r  382  biadan2  443  anbi2ci  446  anbi12i  447  anbi12ci  448  pm5.3  458  an42  551  xchbinx  639  mt2bi  641  orbi12i  713  or42  721  pm5.53  748  orddi  766  anddi  767  pm2.1dc  778  notnotrdc  784  dcim  817  testbitestn  856  rbaib  863  rbaibr  864  pm4.43  890  orbididc  894  pm5.75  903  3orass  922  3anass  923  3ancomb  927  3anan32  930  3anan12  931  anandi3  932  anandi3r  933  xordc  1323  falbitru  1348  19.26-2  1411  19.26-3an  1412  alrot3  1414  albiim  1416  2albiim  1417  19.27h  1492  19.27  1493  19.28h  1494  19.28  1495  nfalt  1510  aaanh  1518  aaan  1519  alinexa  1534  19.21-2  1597  nf2  1598  19.44  1612  19.45  1613  exrot3  1620  exrot4  1621  eeor  1625  sbcof2  1731  sbid2h  1770  19.23vv  1805  sbnv  1809  sblimv  1815  pm11.53  1816  19.41vv  1824  19.41vvv  1825  19.41vvvv  1826  19.42vv  1829  19.42vvv  1830  19.42vvvv  1831  4exdistr  1834  cbvex4v  1846  eean  1847  sbn  1867  sbim  1868  sbor  1869  sban  1870  sbrim  1871  sblim  1872  sbbi  1874  sblbis  1875  sbrbis  1876  sbrbif  1877  sbco2d  1881  sbco2vd  1882  sbnf2  1898  2sb5  1900  2sb6  1901  sbcom2v  1902  sbcom2v2  1903  sbcom2  1904  sb6a  1905  2sb5rf  1906  2sb6rf  1907  sbalyz  1916  sbal  1917  sbal1yz  1918  sbex  1921  sbalv  1922  sbco4lem  1923  exsb  1925  2exsb  1926  eujust  1943  euf  1946  cbveu  1965  mor  1983  eu2  1985  mo4f  2001  eu4  2003  2exeu  2033  2eu4  2034  exists1  2037  abid  2069  eleq12i  2146  abeq2  2187  abeq2i  2189  clabel  2204  abid2f  2243  sbabel  2244  neeq12i  2262  neanior  2332  ralnex  2358  ralinexa  2393  nfraldya  2400  nfrexdya  2401  r3al  2408  r19.26-2  2486  ralbiim  2491  r19.43  2512  ralcomf  2515  rexcomf  2516  rexrot4  2520  reean  2522  3reeanv  2524  rabbi  2531  cbvralf  2571  cbvrexf  2572  cbvreu  2575  cbvral2v  2585  cbvrex2v  2586  cbvral3v  2587  cbvralsv  2588  cbvrexsv  2589  sbralie  2590  rabeq2i  2598  issetf  2606  2gencl  2632  3gencl  2633  ceqsex2  2639  ceqsex3v  2641  ceqsex6v  2643  ceqsex8v  2644  gencbvex  2645  gencbval  2647  spc2gv  2688  eqvincf  2720  ceqsrex2v  2727  elrab2  2751  ralab  2752  ralrab  2753  rexab  2754  rexrab  2755  ralab2  2756  rexab2  2758  eueq3dc  2766  morex  2776  euind  2779  reu2  2780  reu6  2781  rmo4  2785  reu4  2786  reu7  2787  rmoim  2791  2reuswapdc  2794  reuind  2795  2rmorex  2796  sbcco  2836  sbccomlem  2888  sbccom  2889  ra5  2902  rmo3  2905  csbco  2917  sbnfc2  2962  csbabg  2963  cbvralcsf  2964  cbvrexcsf  2965  cbvreucsf  2966  dfss  2987  dfss2f  2990  ss2ab  3062  difeqri  3092  ddifstab  3104  raldifb  3112  uneqri  3114  ssequn2  3145  unss  3146  rexun  3152  ralunb  3153  elin2  3156  ineqri  3159  dfss1  3170  dfss5  3171  ssddif  3198  difin  3201  indif  3207  difundi  3216  indifdir  3220  symdifxor  3230  inrab2  3237  rabun2  3243  reuun2  3247  0el  3268  rabeq0  3274  abeq0  3275  disjr  3293  disj1  3294  undif4  3306  uneqdifeqim  3328  r19.3rm  3330  r19.9rmv  3333  raaan  3347  pwss  3397  dfpr2  3417  ralsnsg  3430  ralsns  3431  eltpg  3438  ralprg  3443  rexprg  3444  raltpg  3445  rextpg  3446  snprc  3457  rabrsndc  3460  euabsn2  3461  eusn  3466  eldifsn  3517  rexdifsn  3521  eqsnm  3547  tpss  3550  snsssn  3553  prel12  3563  preqsn  3567  oprcl  3594  pwtpss  3598  eluniab  3613  elunirab  3614  unipr  3615  dfnfc2  3619  uniun  3620  uniin  3621  uni0b  3626  unissb  3631  elintab  3647  elintrab  3648  ssintab  3653  ssintrab  3659  intun  3667  intpr  3668  elrint  3676  iuncom4  3685  iuneq2  3694  dfiun2g  3710  ssiinf  3727  iundif2ss  3743  elriin  3748  iunxiun  3757  pwssb  3761  iunpwss  3764  dfdisj2  3768  cbvopab1  3851  dftr5  3878  trint  3890  inex1  3912  inuni  3930  repizf2lem  3935  unidif0  3941  axpweq  3945  bnd2  3947  zfpair2  3965  exss  3982  elop  3986  opm  3989  otth  3997  copsex4g  4002  opeqsn  4007  opelopabsbALT  4014  brabga  4019  opelopabaf  4028  iunopab  4036  pwunss  4038  pocl  4058  frirrg  4105  elsuci  4158  elsucg  4159  sucel  4165  unisucg  4169  uniuni  4201  reusv3  4210  iunpw  4229  setindel  4281  elirr  4284  en2lp  4297  ordpwsucss  4310  zfregfr  4316  tfi  4323  peano2  4336  peano5  4339  elxp  4380  opelxp  4392  brxp  4393  rabxp  4398  opthprc  4409  brab2a  4411  opeliunxp  4413  xpundi  4414  xpundir  4415  elvvv  4421  brinxp  4426  brab2ga  4433  0xp  4438  ssrel2  4448  eqrelrel  4459  reliun  4476  reluni  4478  raliunxp  4495  rexiunxp  4496  ralxpf  4500  rexxpf  4501  iunxpf  4502  relop  4504  elcnv  4530  elcnv2  4531  dmin  4561  dmuni  4563  dmopab  4564  dmi  4568  dmmrnm  4572  rnopab  4599  elrnmpt1  4603  rncoeq  4623  resiexg  4673  dfima2  4690  dfima3  4691  elima2  4694  elima3  4695  imai  4701  elimasn  4712  epini  4716  dfse2  4718  cotr  4726  issref  4727  intasym  4729  asymref  4730  cnvopab  4746  cnvi  4748  cnvdif  4750  imainss  4759  rnxpid  4775  dfrel2  4791  dfrel3  4798  dmsnm  4806  rnsnm  4807  relsn2m  4811  dmsnopg  4812  cnvcnvsn  4817  elxp4  4828  elxp5  4829  cnvresima  4830  mptpreima  4834  dfco2  4840  coundi  4842  coundir  4843  imaco  4846  coiun  4850  coi1  4856  relssdmrn  4861  relrelss  4864  unixpm  4873  ressn  4878  cnviinm  4879  cnvpom  4880  cnvsom  4881  cbviota  4892  iotass  4904  dffun2  4932  dffun4  4933  dffun7  4948  dffun8  4949  dffun9  4950  funopab  4955  funun  4964  funcnvsn  4965  fntpg  4975  funcnv2  4979  funcnv  4980  fun2cnv  4983  fncnv  4985  fun11  4986  fununi  4987  imadiflem  4998  imadif  4999  imainlem  5000  funimaexglem  5002  fnunsn  5026  fnres  5035  fnopabg  5042  mptfng  5044  mptun  5049  fun  5083  fcnvres  5093  dff12  5111  f1cnvcnv  5120  funforn  5133  dff1o2  5151  dff1o5  5155  f1orn  5156  resdif  5168  ffoss  5178  f11o  5179  f1o00  5181  fo00  5182  elfv  5196  fv3  5218  nfvres  5227  eqfnfv3  5288  fneqeql  5296  unpreima  5313  respreima  5316  dffo3  5335  dffo5  5337  f1ompt  5341  ffnfvf  5345  fmptco  5351  ftpg  5368  fnressn  5370  idref  5417  abrexco  5419  dff13  5428  dff13f  5430  fliftel  5453  isoini  5477  eusvobj2  5518  acexmidlema  5523  acexmidlemb  5524  acexmidlemph  5525  acexmidlem2  5529  oprabid  5557  brabvv  5571  dfoprab2  5572  eqoprab2b  5583  dmoprab  5605  rnoprab  5607  eloprabga  5611  mpt2mptx  5615  resoprab  5617  ffnov  5625  elrnmpt2  5634  ralrnmpt2  5635  rexrnmpt2  5636  ovid  5637  ovi3  5657  ov6g  5658  foov  5667  opabex3d  5768  opabex3  5769  abexssex  5772  oprabex3  5776  oprabrexex2  5777  fmpt2  5847  xporderlem  5872  f1od2  5876  mpt2xopovel  5879  brtpos2  5889  dmtpos  5894  tpostpos  5902  tpossym  5914  tposoprab  5918  dfsmo2  5925  tfrlem7  5956  tfrlem9  5958  frecabex  6007  el1o  6043  dif1o  6044  dfer2  6130  brdifun  6156  eqerlem  6160  qsid  6194  iinerm  6201  riinerm  6202  erinxp  6203  brecop  6219  eroveu  6220  erovlem  6221  ecopovsym  6225  domen  6255  isfi  6264  en1  6302  xpsnen  6318  xpcomco  6323  xpassen  6327  nneneq  6343  snnen2oprc  6346  ac6sfi  6379  elni  6498  ltexpi  6527  enq0enq  6621  enq0ref  6623  enq0tr  6624  prarloclem3  6687  ltdfpr  6696  genpdflem  6697  genpassl  6714  genpassu  6715  nqprrnd  6733  nqprl  6741  nqpru  6742  ltexprlemopl  6791  ltexprlemopu  6793  ltexprlemdisj  6796  ltexprlemloc  6797  recexprlemdisj  6820  caucvgprprlemell  6875  caucvgprprlemelu  6876  opelcn  6995  elreal  6997  elreal2  6999  peano1nnnn  7020  axicn  7031  axprecex  7046  axpre-ltirr  7048  axpre-mulgt0  7053  axcaucvglemres  7065  xrlenlt  7177  ltxrlt  7178  inelr  7684  reapcotr  7698  1nn  8050  elnnne0  8302  un0addcl  8321  un0mulcl  8322  elnnz  8361  elznn0nn  8365  elznn0  8366  elznn  8367  elz2  8419  zapne  8422  3halfnz  8444  prime  8446  raluz2  8667  rexuz2  8669  supinfneg  8683  infsupneg  8684  eluz2b2  8690  eluz2b3  8691  ublbneg  8698  elq  8707  qreccl  8727  ralrp  8755  rexrp  8756  rpnegap  8766  ltxr  8849  xrnemnf  8853  xrltso  8871  icc0r  8949  divelunit  9024  fzprval  9099  fztpval  9100  elfz1b  9107  4fvwrd4  9150  fzolb  9162  fzolb2  9163  elfzo3  9172  fzouzsplit  9188  elfzo0z  9193  fzo0m  9200  fzind2  9248  ioo0  9268  ico0  9270  ioc0  9271  caucvgre  9867  cvg1nlemcau  9870  resqrexlemex  9911  climeu  10135  divides  10197  fz01or  10278  m1exp1  10301  divalgb  10325  bezoutlemnewy  10385  bezoutlemmain  10387  bezoutlemex  10390  dfgcd2  10403  lcmgcdlem  10459  isprm2  10499  isprm3  10500  isprm4  10501  sqrt2irr  10541  oddpwdc  10552  bdcuni  10667  bdcriota  10674  bdinex1  10690  bj-zfpair2  10701  bj-axun2  10706  bj-ssom  10731