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  2216  necon3bii  2243  ne3anior  2293  r2alf  2341  r2exf  2342  r19.23t  2423  r19.26-3  2443  r19.26m  2444  r19.43  2468  rabid2  2486  isset  2561  ralv  2571  rexv  2572  reuv  2573  rmov  2574  rexcom4b  2579  ceqsex4v  2597  ceqsex8v  2599  ceqsrexv  2674  ralrab2  2706  rexrab2  2708  reu2  2729  reu3  2731  reueq  2738  2reuswapdc  2743  reuind  2744  rmo2ilem  2847  dfss2  2934  dfss3  2935  dfss3f  2937  ssabral  3011  rabss  3017  ssrabeq  3026  uniiunlem  3028  uncom  3087  inass  3147  nsspssun  3170  indi  3184  difindiss  3191  difin2  3199  reupick3  3222  n0rf  3233  eq0  3239  eqv  3240  vss  3264  disj  3268  disj3  3272  undisj1  3279  undisj2  3280  exsnrex  3413  euabsn2  3439  euabsn  3440  prssg  3521  dfuni2  3582  unissb  3610  elint2  3622  ssint  3631  dfiin2g  3690  iunn0m  3717  iunxun  3735  iunxiun  3736  iinpw  3742  dftr2  3856  dftr5  3857  dftr3  3858  dftr4  3859  vprc  3888  inuni  3909  snelpw  3949  sspwb  3952  opelopabsb  3997  eusv2  4189  orddif  4271  onintexmid  4297  zfregfr  4298  tfi  4305  opthprc  4391  elxp3  4394  xpiundir  4399  elvv  4402  brinxp2  4407  relsn  4443  reliun  4458  inxp  4470  raliunxp  4477  rexiunxp  4478  cnvuni  4521  dm0rn0  4552  elrn  4577  ssdmres  4633  dfres2  4658  dfima2  4670  args  4694  cotr  4706  intasym  4709  asymref  4710  intirr  4711  cnv0  4727  xp11m  4759  cnvresima  4810  resco  4825  rnco  4827  coiun  4830  coass  4839  dfiota2  4868  dffun2  4912  dffun6f  4915  dffun4f  4918  dffun7  4928  dffun9  4930  funfn  4931  svrelfun  4964  imadiflem  4978  dffn2  5047  dffn3  5053  fintm  5075  dffn4  5112  dff1o4  5134  brprcneu  5171  eqfnfv3  5267  fnreseql  5277  fsn  5335  abrexco  5398  imaiun  5399  mpt22eqb  5610  elovmpt2  5701  abexex  5753  releldm2  5811  fnmpt2  5828  dftpos4  5878  tfrlem7  5933  0er  6140  eroveu  6197  erovlem  6198  domen  6232  reuen1  6281  ssfiexmid  6336  dmaddpq  6477  dmmulpq  6478  distrnqg  6485  enq0enq  6529  enq0tr  6532  nqnq0pi  6536  distrnq0  6557  prltlu  6585  prarloc  6601  genpdflem  6605  ltexprlemm  6698  ltexprlemlol  6700  ltexprlemupu  6702  ltexprlemdisj  6704  recexprlemdisj  6728  ltresr  6915  elnnz  8255  dfz2  8313  2rexuz  8525  eluz2b1  8539  elxr  8696  elixx1  8766  elioo2  8790  elioopnf  8836  elicopnf  8838  elfz1  8879  fzdifsuc  8943  fznn  8951  fzp1nel  8966  fznn0  8974  redivap  9474  imdivap  9481  climreu  9818  dcdc  9901  bj-vprc  10016