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

Step	Hyp	Ref	Expression
1		bitri.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 119	. . 3 ⊢ (𝜑 → 𝜓)
3		bitri.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
4	2, 3	sylib 121	. 2 ⊢ (𝜑 → 𝜒)
5	3	biimpri 132	. . 3 ⊢ (𝜒 → 𝜓)
6	5, 1	sylibr 133	. 2 ⊢ (𝜒 → 𝜑)
7	4, 6	impbii 125	1 ⊢ (𝜑 ↔ 𝜒)

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  387  biadan2  451  anbi2ci  454  anbi12i  455  anbi12ci  456  pm5.3  466  an42  576  xchbinx  671  mt2bi  673  orbi12i  753  or42  761  pm5.53  791  orddi  809  anddi  810  pm2.1dc  822  dcim  826  notnotrdc  828  dcnnOLD  834  rbaib  906  rbaibr  907  pm4.43  933  orbididc  937  pm5.75  946  3orass  965  3anass  966  3ancomb  970  3anan32  973  3anan12  974  anandi3  975  anandi3r  976  xordc  1370  falbitru  1395  19.26-2  1458  19.26-3an  1459  alrot3  1461  albiim  1463  2albiim  1464  19.27h  1539  19.27  1540  19.28h  1541  19.28  1542  nfalt  1557  aaanh  1565  aaan  1566  alinexa  1582  19.21-2  1645  nf2  1646  19.44  1660  19.45  1661  exrot3  1668  exrot4  1669  eeor  1673  sbcof2  1782  sbid2h  1821  19.23vv  1856  sbnv  1860  sblimv  1866  pm11.53  1867  19.41vv  1875  19.41vvv  1876  19.41vvvv  1877  exdistrv  1882  19.42vv  1883  19.42vvv  1884  19.42vvvv  1885  4exdistr  1888  cbvex4v  1900  eean  1901  sbn  1923  sbim  1924  sbor  1925  sban  1926  sbrim  1927  sblim  1928  sbbi  1930  sblbis  1931  sbrbis  1932  sbrbif  1933  sbco2d  1937  sbco2vd  1938  sbnf2  1954  2sb5  1956  2sb6  1957  sbcom2v  1958  sbcom2v2  1959  sbcom2  1960  sb6a  1961  2sb5rf  1962  2sb6rf  1963  sbalyz  1972  sbal  1973  sbal1yz  1974  sbex  1977  sbalv  1978  sbco4lem  1979  exsb  1981  2exsb  1982  eujust  1999  euf  2002  cbveu  2021  mor  2039  eu2  2041  mo4f  2057  eu4  2059  2exeu  2089  2eu4  2090  exists1  2093  abid  2125  eleq12i  2205  abeq2  2246  abeq2i  2248  clabel  2264  abid2f  2304  sbabel  2305  neeq12i  2323  neanior  2393  ralnex  2424  dfrex2dc  2426  ralinexa  2460  nfraldya  2467  nfrexdya  2468  r3al  2475  r19.26-2  2559  ralbiim  2564  ralnex2  2569  r19.43  2587  ralcomf  2590  rexcomf  2591  rexrot4  2595  reean  2597  3reeanv  2599  rabbi  2606  cbvralf  2646  cbvrexf  2647  cbvreu  2650  cbvral2v  2660  cbvrex2v  2661  cbvral3v  2662  cbvralsv  2663  cbvrexsv  2664  sbralie  2665  rabeq2i  2678  issetf  2688  2gencl  2714  3gencl  2715  ceqsex2  2721  ceqsex3v  2723  ceqsex6v  2725  ceqsex8v  2726  gencbvex  2727  gencbval  2729  spc2gv  2771  eqvincf  2805  ceqsrex2v  2812  elrab2  2838  ralab  2839  ralrab  2840  rexab  2841  rexrab  2842  ralab2  2843  rexab2  2845  eueq3dc  2853  morex  2863  euind  2866  reu2  2867  reu6  2868  rmo4  2872  reu4  2873  reu7  2874  rmo3f  2876  rmo4f  2877  rmoim  2880  2reuswapdc  2883  reuind  2884  2rmorex  2885  sbcco  2925  sbccomlem  2978  sbccom  2979  ra5  2992  rmo3  2995  csbco  3008  sbnfc2  3055  csbabg  3056  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  dfss  3080  dfss2f  3083  ss2ab  3160  dfdif3  3181  difeqri  3191  ddifstab  3203  raldifb  3211  uneqri  3213  ssequn2  3244  unss  3245  rexun  3251  ralunb  3252  elin2  3259  ineqri  3264  dfss1  3275  dfss5  3276  dfss4st  3304  ssddif  3305  difin  3308  indif  3314  difundi  3323  indifdir  3327  symdifxor  3337  inrab2  3344  rabun2  3350  reuun2  3354  0el  3380  rabeq0  3387  abeq0  3388  disjr  3407  disj1  3408  undif4  3420  uneqdifeqim  3443  r19.2m  3444  r19.3rm  3446  r19.9rmv  3449  raaan  3464  pwss  3521  dfpr2  3541  ralsnsg  3556  ralsns  3557  eltpg  3564  ralprg  3569  rexprg  3570  raltpg  3571  rextpg  3572  snprc  3583  rabrsndc  3586  euabsn2  3587  eusn  3592  eldifsn  3645  ssdifsn  3646  rexdifsn  3650  eqsnm  3677  tpss  3680  snsssn  3683  prel12  3693  preqsn  3697  oprcl  3724  pwtpss  3728  eluniab  3743  elunirab  3744  unipr  3745  dfnfc2  3749  uniun  3750  uniin  3751  uni0b  3756  unissb  3761  elintab  3777  elintrab  3778  ssintab  3783  ssintrab  3789  intun  3797  intpr  3798  elrint  3806  iuncom4  3815  iuneq2  3824  dfiun2g  3840  ssiinf  3857  iundif2ss  3873  elriin  3878  iunxiun  3889  pwssb  3893  elpwpw  3894  iunpwss  3899  dfdisj2  3903  disjiun  3919  cbvopab1  3996  dftr5  4024  trint  4036  inex1  4057  inuni  4075  repizf2lem  4080  unidif0  4086  axpweq  4090  bnd2  4092  exmid01  4116  zfpair2  4127  exss  4144  elop  4148  opm  4151  otth  4159  copsex4g  4164  opeqsn  4169  opelopabsbALT  4176  brabga  4181  opelopabaf  4190  iunopab  4198  pwunss  4200  pocl  4220  frirrg  4267  elsuci  4320  elsucg  4321  sucel  4327  unisucg  4331  uniuni  4367  reusv3  4376  iunpw  4396  setindel  4448  elirr  4451  en2lp  4464  ordpwsucss  4477  zfregfr  4483  tfi  4491  peano2  4504  peano5  4507  elxp  4551  opelxp  4564  brxp  4565  rabxp  4571  opthprc  4585  brab2a  4587  opeliunxp  4589  xpundi  4590  xpundir  4591  elvvv  4597  brinxp  4602  brab2ga  4609  0xp  4614  ssrel2  4624  eqrelrel  4635  reliun  4655  reluni  4657  raliunxp  4675  rexiunxp  4676  ralxpf  4680  rexxpf  4681  iunxpf  4682  relop  4684  elco  4700  elcnv  4711  elcnv2  4712  dmin  4742  dmuni  4744  dmopab  4745  dmi  4749  dmmrnm  4753  rnopab  4781  elrnmpt1  4785  rncoeq  4807  resiexg  4859  dfima2  4878  dfima3  4879  elima2  4882  elima3  4883  imai  4890  elimasn  4901  epini  4905  dfse2  4907  cotr  4915  issref  4916  intasym  4918  asymref  4919  cnvopab  4935  cnvi  4938  cnvdif  4940  imainss  4949  rnxpid  4968  dfrel2  4984  dfrel3  4991  dmsnm  4999  rnsnm  5000  relsn2m  5004  dmsnopg  5005  cnvcnvsn  5010  elxp4  5021  elxp5  5022  cnvresima  5023  mptpreima  5027  dfco2  5033  coundi  5035  coundir  5036  imaco  5039  coiun  5043  coi1  5049  relssdmrn  5054  relrelss  5060  unixpm  5069  ressn  5074  cnviinm  5075  cnvpom  5076  cnvsom  5077  cbviota  5088  iotass  5100  dffun2  5128  dffun4  5129  dffun7  5145  dffun8  5146  dffun9  5147  funopab  5153  funun  5162  funcnvsn  5163  fntpg  5174  funcnv2  5178  funcnv  5179  fun2cnv  5182  fncnv  5184  fun11  5185  fununi  5186  imadiflem  5197  imadif  5198  imainlem  5199  funimaexglem  5201  fnunsn  5225  fnres  5234  fnopabg  5241  mptfng  5243  mptun  5249  fun  5290  fcnvres  5301  dff12  5322  f1cnvcnv  5334  funforn  5347  dff1o2  5365  dff1o5  5369  f1orn  5370  resdif  5382  ffoss  5392  f11o  5393  f1o00  5395  fo00  5396  elfv  5412  fv3  5437  nfvres  5447  eqfnfv3  5513  fneqeql  5521  unpreima  5538  respreima  5541  dffo3  5560  dffo5  5562  f1ompt  5564  ffnfvf  5572  fmptco  5579  ftpg  5597  fnressn  5599  idref  5651  abrexco  5653  dff13  5662  dff13f  5664  fliftel  5687  isoini  5712  eusvobj2  5753  acexmidlema  5758  acexmidlemb  5759  acexmidlemph  5760  acexmidlem2  5764  oprabid  5796  brabvv  5810  dfoprab2  5811  eqoprab2b  5822  dmoprab  5845  rnoprab  5847  eloprabga  5851  mpomptx  5855  resoprab  5860  ffnov  5868  elrnmpo  5877  ralrnmpo  5878  rexrnmpo  5879  ovid  5880  ovi3  5900  ov6g  5901  foov  5910  opabex3d  6012  opabex3  6013  abexssex  6016  oprabex3  6020  oprabrexex2  6021  fmpo  6092  xporderlem  6121  f1od2  6125  mpoxopovel  6131  brtpos2  6141  dmtpos  6146  tpostpos  6154  tpossym  6166  tposoprab  6170  dfsmo2  6177  tfrlem7  6207  tfrlem9  6209  tfr1onlemaccex  6238  tfrcllemaccex  6251  tfrcldm  6253  frecabex  6288  el1o  6327  dif1o  6328  dfer2  6423  brdifun  6449  eqerlem  6453  qsid  6487  iinerm  6494  riinerm  6495  erinxp  6496  brecop  6512  eroveu  6513  erovlem  6514  ecopovsym  6518  mapval2  6565  mapsn  6577  elixp  6592  ixpeq2  6599  ixpin  6610  ixpiinm  6611  mptelixpg  6621  ixpsnf1o  6623  domen  6638  isfi  6648  en1  6686  xpsnen  6708  xpcomco  6713  xpassen  6717  ssenen  6738  nneneq  6744  snnen2oprc  6747  ac6sfi  6785  exmidpw  6795  eldju  6946  djur  6947  eldju2ndl  6950  eldju2ndr  6951  finomni  7005  acfun  7056  ccfunen  7072  elni  7109  ltexpi  7138  enq0enq  7232  enq0ref  7234  enq0tr  7235  prarloclem3  7298  ltdfpr  7307  genpdflem  7308  genpassl  7325  genpassu  7326  nqprrnd  7344  nqprl  7352  nqpru  7353  ltexprlemopl  7402  ltexprlemopu  7404  ltexprlemdisj  7407  ltexprlemloc  7408  recexprlemdisj  7431  caucvgprprlemell  7486  caucvgprprlemelu  7487  suplocexprlemml  7517  suplocsrlemb  7607  opelcn  7627  elreal  7629  elreal2  7631  peano1nnnn  7653  axicn  7664  axaddf  7669  axmulf  7670  axprecex  7681  axpre-ltirr  7683  axpre-mulgt0  7688  axcaucvglemres  7700  axpre-suploc  7703  xrlenlt  7822  ltxrlt  7823  inelr  8339  reapcotr  8353  1nn  8724  elnnne0  8984  un0addcl  9003  un0mulcl  9004  elnnz  9057  elznn0nn  9061  elznn0  9062  elznn  9063  elz2  9115  zapne  9118  3halfnz  9141  prime  9143  raluz2  9367  rexuz2  9369  supinfneg  9383  infsupneg  9384  eluz2b2  9390  eluz2b3  9391  ublbneg  9398  elq  9407  qreccl  9427  ralrp  9456  rexrp  9457  rpnegap  9467  ltxr  9555  xrnemnf  9557  xrltso  9575  icc0r  9702  divelunit  9778  fzprval  9855  fztpval  9856  elfz1b  9863  fz01or  9884  4fvwrd4  9910  fzolb  9923  fzolb2  9924  elfzo3  9933  fzouzsplit  9949  elfzo0z  9954  fzo0m  9961  fzind2  10009  ioo0  10030  ico0  10032  ioc0  10033  uzennn  10202  seq3f1olemp  10268  caucvgre  10746  cvg1nlemcau  10749  resqrexlemex  10790  climeu  11058  fsum2dlemstep  11196  expcnv  11266  divides  11484  m1exp1  11587  divalgb  11611  bezoutlemnewy  11673  bezoutlemmain  11675  bezoutlemex  11678  dfgcd2  11691  lcmgcdlem  11747  isprm2  11787  isprm3  11788  isprm4  11789  sqrt2irr  11829  oddpwdc  11841  ennnfoneleminc  11913  ennnfonelemex  11916  ennnfonelemr  11925  ctiunct  11942  istps  12188  istps2  12189  isbasis2g  12201  tgval2  12209  txuni2  12414  tx1cn  12427  tx2cn  12428  uptx  12432  txdis1cn  12436  blres  12592  xmeterval  12593  xmeter  12594  isxms2  12610  isms2  12612  metrest  12664  qtopbasss  12679  dedekindicclemicc  12768  limcdifap  12789  pilem1  12849  sincosq1lem  12895  decidr  12992  bdcuni  13063  bdcriota  13070  bdinex1  13086  bj-zfpair2  13097  bj-axun2  13102  bj-ssom  13123  ss1oel2o  13178  nninfsellemdc  13195  nninfsellemsuc  13197  nninfsellemqall  13200