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  421  mpbiran  836  mpbiran2  837  3anrev  886  an6  1204  nfand  1444  19.33b2  1504  nf3  1541  nf4dc  1542  nf4r  1543  equsalh  1596  sb6x  1645  sb5f  1668  sbidm  1715  sb5  1751  sbanv  1753  sborv  1754  sbhb  1798  sb3an  1814  sbel2x  1856  sbal1yz  1859  sbexyz  1861  eu2  1926  2eu4  1976  cleqh  2120  cleqf  2184  necon3bii  2220  ne3anior  2270  r2alf  2318  r2exf  2319  r19.23t  2400  r19.26-3  2420  r19.26m  2421  r19.43  2445  rabid2  2463  isset  2538  ralv  2547  rexv  2548  reuv  2549  rmov  2550  rexcom4b  2555  ceqsex4v  2573  ceqsex8v  2575  ceqsrexv  2650  ralrab2  2682  rexrab2  2684  reu2  2705  reu3  2707  reueq  2714  2reuswapdc  2719  reuind  2720  rmo2ilem  2824  dfss2  2913  dfss3  2914  dfss3f  2916  ssabral  2990  rabss  2996  ssrabeq  3005  uniiunlem  3007  uncom  3066  inass  3126  nsspssun  3149  indi  3163  difindiss  3170  difin2  3178  reupick3  3201  n0rf  3212  eq0  3218  eqv  3219  vss  3243  disj  3247  disj3  3251  undisj1  3258  undisj2  3259  exsnrex  3365  euabsn2  3391  euabsn  3392  prssg  3473  dfuni2  3535  unissb  3563  elint2  3575  ssint  3584  dfiin2g  3643  iunn0m  3670  iunxun  3688  iunxiun  3689  iinpw  3695  dftr2  3809  dftr5  3810  dftr3  3811  dftr4  3812  vprc  3841  inuni  3862  snelpw  3902  sspwb  3905  opelopabsb  3951  eusv2  4115  tfi  4208  opthprc  4294  elxp3  4297  xpiundir  4302  elvv  4305  brinxp2  4310  relsn  4346  reliun  4361  inxp  4373  raliunxp  4380  rexiunxp  4381  cnvuni  4424  dm0rn0  4455  elrn  4480  ssdmres  4537  dfres2  4562  dfima2  4574  args  4598  cotr  4610  intasym  4613  asymref  4614  intirr  4615  cnv0  4631  xp11m  4663  cnvresima  4714  resco  4729  rnco  4731  coiun  4734  coass  4743  dfiota2  4772  dffun2  4816  dffun6f  4818  dffun4f  4821  dffun7  4831  dffun9  4833  funfn  4834  svrelfun  4867  imadiflem  4881  dffn2  4950  dffn3  4956  fintm  4977  dffn4  5014  dff1o4  5036  brprcneu  5073  eqfnfv3  5169  fnreseql  5179  fsn  5237  abrexco  5300  imaiun  5301  mpt22eqb  5512  elovmpt2  5600  abexex  5652  releldm2  5710  fnmpt2  5727  dftpos4  5776  tfrlem7  5830  0er  6023  eroveu  6078  erovlem  6079