Theorem bitr4i 176

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr4i.1	⊢ (𝜑 ↔ 𝜓)
bitr4i.2	⊢ (𝜒 ↔ 𝜓)

Assertion

Ref	Expression
bitr4i	⊢ (𝜑 ↔ 𝜒)

Proof of Theorem bitr4i

Step	Hyp	Ref	Expression
1		bitr4i.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		bitr4i.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	2	bicomi 123	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	bitri 173	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3bitr2i  197  3bitr2ri  198  3bitr4i  201  3bitr4ri  202  imdistan  418  mpbiran  847  mpbiran2  848  3anrev  895  an6  1216  nfand  1460  19.33b2  1520  nf3  1559  nf4dc  1560  nf4r  1561  equsalh  1614  sb6x  1662  sb5f  1685  sbidm  1731  sb5  1767  sbanv  1769  sborv  1770  sbhb  1816  sb3an  1832  sbel2x  1874  sbal1yz  1877  sbexyz  1879  eu2  1944  2eu4  1993  cleqh  2137  cleqf  2201  dcne  2214  necon3bii  2240  ne3anior  2290  r2alf  2338  r2exf  2339  r19.23t  2420  r19.26-3  2440  r19.26m  2441  r19.43  2465  rabid2  2483  isset  2558  ralv  2568  rexv  2569  reuv  2570  rmov  2571  rexcom4b  2576  ceqsex4v  2594  ceqsex8v  2596  ceqsrexv  2671  ralrab2  2703  rexrab2  2705  reu2  2726  reu3  2728  reueq  2735  2reuswapdc  2740  reuind  2741  rmo2ilem  2844  dfss2  2931  dfss3  2932  dfss3f  2934  ssabral  3008  rabss  3014  ssrabeq  3023  uniiunlem  3025  uncom  3084  inass  3144  nsspssun  3167  indi  3181  difindiss  3188  difin2  3196  reupick3  3219  n0rf  3230  eq0  3236  eqv  3237  vss  3261  disj  3265  disj3  3269  undisj1  3276  undisj2  3277  exsnrex  3410  euabsn2  3436  euabsn  3437  prssg  3518  dfuni2  3579  unissb  3607  elint2  3619  ssint  3628  dfiin2g  3687  iunn0m  3714  iunxun  3732  iunxiun  3733  iinpw  3739  dftr2  3853  dftr5  3854  dftr3  3855  dftr4  3856  vprc  3885  inuni  3906  snelpw  3946  sspwb  3949  opelopabsb  3994  eusv2  4176  orddif  4256  onintexmid  4282  tfi  4283  opthprc  4369  elxp3  4372  xpiundir  4377  elvv  4380  brinxp2  4385  relsn  4421  reliun  4436  inxp  4448  raliunxp  4455  rexiunxp  4456  cnvuni  4499  dm0rn0  4530  elrn  4555  ssdmres  4611  dfres2  4636  dfima2  4648  args  4672  cotr  4684  intasym  4687  asymref  4688  intirr  4689  cnv0  4705  xp11m  4737  cnvresima  4788  resco  4803  rnco  4805  coiun  4808  coass  4817  dfiota2  4846  dffun2  4890  dffun6f  4893  dffun4f  4896  dffun7  4906  dffun9  4908  funfn  4909  svrelfun  4942  imadiflem  4956  dffn2  5025  dffn3  5031  fintm  5053  dffn4  5090  dff1o4  5112  brprcneu  5149  eqfnfv3  5245  fnreseql  5255  fsn  5313  abrexco  5376  imaiun  5377  mpt22eqb  5588  elovmpt2  5679  abexex  5731  releldm2  5789  fnmpt2  5806  dftpos4  5856  tfrlem7  5911  0er  6118  eroveu  6175  erovlem  6176  domen  6210  reuen1  6259  ssfiexmid  6314  dmaddpq  6449  dmmulpq  6450  distrnqg  6457  enq0enq  6501  enq0tr  6504  nqnq0pi  6508  distrnq0  6529  prltlu  6557  prarloc  6573  genpdflem  6577  ltexprlemm  6670  ltexprlemlol  6672  ltexprlemupu  6674  ltexprlemdisj  6676  recexprlemdisj  6700  ltresr  6887  elnnz  8218  dfz2  8276  2rexuz  8488  eluz2b1  8502  elxr  8654  elixx1  8724  elioo2  8748  elioopnf  8794  elicopnf  8796  elfz1  8837  fzdifsuc  8901  fznn  8909  fzp1nel  8924  fznn0  8932  redivap  9343  imdivap  9350  climreu  9686  dcdc  9765  bj-vprc  9880