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  835  mpbiran2  836  3anrev  883  an6  1201  nfand  1442  19.33b2  1502  nf3  1541  nf4dc  1542  nf4r  1543  equsalh  1596  sb6x  1644  sb5f  1667  sbidm  1713  sb5  1749  sbanv  1751  sborv  1752  sbhb  1798  sb3an  1814  sbel2x  1856  sbal1yz  1859  sbexyz  1861  eu2  1926  2eu4  1975  cleqh  2119  cleqf  2183  necon3bii  2221  ne3anior  2271  r2alf  2319  r2exf  2320  r19.23t  2401  r19.26-3  2421  r19.26m  2422  r19.43  2446  rabid2  2464  isset  2539  ralv  2548  rexv  2549  reuv  2550  rmov  2551  rexcom4b  2556  ceqsex4v  2574  ceqsex8v  2576  ceqsrexv  2651  ralrab2  2683  rexrab2  2685  reu2  2706  reu3  2708  reueq  2715  2reuswapdc  2720  reuind  2721  rmo2ilem  2824  dfss2  2911  dfss3  2912  dfss3f  2914  ssabral  2988  rabss  2994  ssrabeq  3003  uniiunlem  3005  uncom  3064  inass  3124  nsspssun  3147  indi  3161  difindiss  3168  difin2  3176  reupick3  3199  n0rf  3210  eq0  3216  eqv  3217  vss  3241  disj  3245  disj3  3249  undisj1  3256  undisj2  3257  exsnrex  3387  euabsn2  3413  euabsn  3414  prssg  3495  dfuni2  3556  unissb  3584  elint2  3596  ssint  3605  dfiin2g  3664  iunn0m  3691  iunxun  3709  iunxiun  3710  iinpw  3716  dftr2  3830  dftr5  3831  dftr3  3832  dftr4  3833  vprc  3862  inuni  3883  snelpw  3923  sspwb  3926  opelopabsb  3971  eusv2  4139  tfi  4232  opthprc  4318  elxp3  4321  xpiundir  4326  elvv  4329  brinxp2  4334  relsn  4370  reliun  4385  inxp  4397  raliunxp  4404  rexiunxp  4405  cnvuni  4448  dm0rn0  4479  elrn  4504  ssdmres  4560  dfres2  4585  dfima2  4597  args  4621  cotr  4633  intasym  4636  asymref  4637  intirr  4638  cnv0  4654  xp11m  4686  cnvresima  4737  resco  4752  rnco  4754  coiun  4757  coass  4766  dfiota2  4795  dffun2  4839  dffun6f  4841  dffun4f  4844  dffun7  4854  dffun9  4856  funfn  4857  svrelfun  4890  imadiflem  4904  dffn2  4973  dffn3  4979  fintm  5000  dffn4  5037  dff1o4  5059  brprcneu  5096  eqfnfv3  5192  fnreseql  5202  fsn  5260  abrexco  5323  imaiun  5324  mpt22eqb  5533  elovmpt2  5624  abexex  5676  releldm2  5734  fnmpt2  5751  dftpos4  5800  tfrlem7  5855  0er  6051  eroveu  6108  erovlem  6109  dmaddpq  6238  dmmulpq  6239  distrnqg  6246  enq0enq  6286  enq0tr  6289  nqnq0pi  6293  distrnq0  6314  prltlu  6341  prarloc  6357  genpdflem  6361  ltexprlemm  6437  ltexprlemlol  6439  ltexprlemupu  6441  ltexprlemdisj  6443  recexprlemdisj  6464  ltresr  6550  dcdc  7007  bj-df-test  7008  bj-vprc  7119