Theorem bitr4i 186

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 131	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	bitri 183	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitr2i  207  3bitr2ri  208  3bitr4i  211  3bitr4ri  212  biancomi  268  imdistan  440  biadani  601  mpbiran  924  mpbiran2  925  3anrev  972  an6  1299  nfand  1547  19.33b2  1608  nf3  1647  nf4dc  1648  nf4r  1649  equsalh  1704  sb6x  1752  sb5f  1776  sbidm  1823  sb5  1859  sbanv  1861  sborv  1862  sbhb  1911  sb3an  1929  sbel2x  1971  sbal1yz  1974  sbexyz  1976  eu2  2041  2eu4  2090  cleqh  2237  cleqf  2303  dcne  2317  necon3bii  2344  ne3anior  2394  r2alf  2450  r2exf  2451  r19.23t  2537  r19.26-3  2560  r19.26m  2561  r19.43  2587  rabid2  2605  isset  2687  ralv  2698  rexv  2699  reuv  2700  rmov  2701  rexcom4b  2706  ceqsex4v  2724  ceqsex8v  2726  ceqsrexv  2810  ralrab2  2844  rexrab2  2846  reu2  2867  reu3  2869  reueq  2878  2reuswapdc  2883  reuind  2884  sbc3an  2965  rmo2ilem  2993  dfss2  3081  dfss3  3082  dfss3f  3084  ssabral  3163  rabss  3169  ssrabeq  3178  uniiunlem  3180  dfdif3  3181  ddifstab  3203  uncom  3215  inass  3281  indi  3318  difindiss  3325  difin2  3333  reupick3  3356  n0rf  3370  eq0  3376  eqv  3377  vss  3405  disj  3406  disj3  3410  undisj1  3415  undisj2  3416  exsnrex  3561  euabsn2  3587  euabsn  3588  prssg  3672  dfuni2  3733  unissb  3761  elint2  3773  ssint  3782  dfiin2g  3841  iunn0m  3868  iunxun  3887  iunxiun  3889  iinpw  3898  disjnim  3915  dftr2  4023  dftr5  4024  dftr3  4025  dftr4  4026  vnex  4054  inuni  4075  snelpw  4130  sspwb  4133  opelopabsb  4177  eusv2  4373  orddif  4457  onintexmid  4482  zfregfr  4483  tfi  4491  opthprc  4585  elxp3  4588  xpiundir  4593  elvv  4596  brinxp2  4601  relsn  4639  reliun  4655  inxp  4668  raliunxp  4675  rexiunxp  4676  cnvuni  4720  dm0rn0  4751  elrn  4777  ssdmres  4836  dfres2  4866  dfima2  4878  args  4903  cotr  4915  intasym  4918  asymref  4919  intirr  4920  cnv0  4937  xp11m  4972  cnvresima  5023  resco  5038  rnco  5040  coiun  5043  coass  5052  dfiota2  5084  dffun2  5128  dffun6f  5131  dffun4f  5134  dffun7  5145  dffun9  5147  funfn  5148  svrelfun  5183  imadiflem  5197  dffn2  5269  dffn3  5278  fintm  5303  dffn4  5346  dff1o4  5368  brprcneu  5407  eqfnfv3  5513  fnreseql  5523  fsn  5585  abrexco  5653  imaiun  5654  mpo2eqb  5873  elovmpo  5964  abexex  6017  releldm2  6076  fnmpo  6093  dftpos4  6153  tfrlem7  6207  0er  6456  eroveu  6513  erovlem  6514  map0e  6573  elixpconst  6593  domen  6638  reuen1  6688  xpf1o  6731  ssfilem  6762  finexdc  6789  ssfirab  6815  sbthlemi10  6847  djuexb  6922  dmaddpq  7180  dmmulpq  7181  distrnqg  7188  enq0enq  7232  enq0tr  7235  nqnq0pi  7239  distrnq0  7260  prltlu  7288  prarloc  7304  genpdflem  7308  ltexprlemm  7401  ltexprlemlol  7403  ltexprlemupu  7405  ltexprlemdisj  7407  recexprlemdisj  7431  ltresr  7640  elnnz  9057  dfz2  9116  2rexuz  9370  eluz2b1  9388  elxr  9556  elixx1  9673  elioo2  9697  elioopnf  9743  elicopnf  9745  elfz1  9788  fzdifsuc  9854  fznn  9862  fzp1nel  9877  fznn0  9886  redivap  10639  imdivap  10646  rexanre  10985  climreu  11059  3dvdsdec  11551  3dvds2dec  11552  bezoutlembi  11682  isprm2  11787  isprm3  11788  isprm4  11789  inffinp1  11931  isbasis3g  12202  restsn  12338  lmbr  12371  txbas  12416  tx2cn  12428  elcncf1di  12724  dedekindicclemicc  12768  limcrcl  12785  bj-nnor  12935  bj-vprc  13083  ss1oel2o  13178  subctctexmid  13185