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  846  mpbiran2  847  3anrev  894  an6  1215  nfand  1457  19.33b2  1517  nf3  1556  nf4dc  1557  nf4r  1558  equsalh  1611  sb6x  1659  sb5f  1682  sbidm  1728  sb5  1764  sbanv  1766  sborv  1767  sbhb  1813  sb3an  1829  sbel2x  1871  sbal1yz  1874  sbexyz  1876  eu2  1941  2eu4  1990  cleqh  2134  cleqf  2198  dcne  2211  necon3bii  2237  ne3anior  2287  r2alf  2335  r2exf  2336  r19.23t  2417  r19.26-3  2437  r19.26m  2438  r19.43  2462  rabid2  2480  isset  2555  ralv  2565  rexv  2566  reuv  2567  rmov  2568  rexcom4b  2573  ceqsex4v  2591  ceqsex8v  2593  ceqsrexv  2668  ralrab2  2700  rexrab2  2702  reu2  2723  reu3  2725  reueq  2732  2reuswapdc  2737  reuind  2738  rmo2ilem  2841  dfss2  2928  dfss3  2929  dfss3f  2931  ssabral  3005  rabss  3011  ssrabeq  3020  uniiunlem  3022  uncom  3081  inass  3141  nsspssun  3164  indi  3178  difindiss  3185  difin2  3193  reupick3  3216  n0rf  3227  eq0  3233  eqv  3234  vss  3258  disj  3262  disj3  3266  undisj1  3273  undisj2  3274  exsnrex  3404  euabsn2  3430  euabsn  3431  prssg  3512  dfuni2  3573  unissb  3601  elint2  3613  ssint  3622  dfiin2g  3681  iunn0m  3708  iunxun  3726  iunxiun  3727  iinpw  3733  dftr2  3847  dftr5  3848  dftr3  3849  dftr4  3850  vprc  3879  inuni  3900  snelpw  3940  sspwb  3943  opelopabsb  3988  eusv2  4155  tfi  4248  opthprc  4334  elxp3  4337  xpiundir  4342  elvv  4345  brinxp2  4350  relsn  4386  reliun  4401  inxp  4413  raliunxp  4420  rexiunxp  4421  cnvuni  4464  dm0rn0  4495  elrn  4520  ssdmres  4576  dfres2  4601  dfima2  4613  args  4637  cotr  4649  intasym  4652  asymref  4653  intirr  4654  cnv0  4670  xp11m  4702  cnvresima  4753  resco  4768  rnco  4770  coiun  4773  coass  4782  dfiota2  4811  dffun2  4855  dffun6f  4858  dffun4f  4861  dffun7  4871  dffun9  4873  funfn  4874  svrelfun  4907  imadiflem  4921  dffn2  4990  dffn3  4996  fintm  5018  dffn4  5055  dff1o4  5077  brprcneu  5114  eqfnfv3  5210  fnreseql  5220  fsn  5278  abrexco  5341  imaiun  5342  mpt22eqb  5552  elovmpt2  5643  abexex  5695  releldm2  5753  fnmpt2  5770  dftpos4  5819  tfrlem7  5874  0er  6076  eroveu  6133  erovlem  6134  domen  6168  reuen1  6217  ssfiexmid  6254  dmaddpq  6363  dmmulpq  6364  distrnqg  6371  enq0enq  6413  enq0tr  6416  nqnq0pi  6420  distrnq0  6441  prltlu  6469  prarloc  6485  genpdflem  6489  ltexprlemm  6573  ltexprlemlol  6575  ltexprlemupu  6577  ltexprlemdisj  6579  recexprlemdisj  6601  ltresr  6716  elnnz  8011  dfz2  8069  2rexuz  8281  eluz2b1  8295  elxr  8446  elixx1  8516  elioo2  8540  elioopnf  8586  elicopnf  8588  elfz1  8629  fzdifsuc  8693  fznn  8701  fzp1nel  8716  fznn0  8724  redivap  9082  imdivap  9089  dcdc  9216  bj-vprc  9327