Theorem bitr4i 187

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

Syntax hints:   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitr2i  208  3bitr2ri  209  3bitr4i  212  3bitr4ri  213  biancomi  270  imdistan  444  bianass  469  biadani  612  mpbiran  942  mpbiran2  943  3anrev  990  an6  1332  nfand  1579  19.33b2  1640  nf3  1680  nf4dc  1681  nf4r  1682  equsalh  1737  sb6x  1790  sb5f  1815  sbidm  1862  sb5  1899  sbanv  1901  sborv  1902  sbhb  1956  sb3an  1974  sbel2x  2014  sbal1yz  2017  sbexyz  2019  eu2  2086  2eu4  2135  cleqh  2293  cleqf  2361  dcne  2375  necon3bii  2402  ne3anior  2452  r2alf  2511  r2exf  2512  r19.23t  2601  r19.26-3  2624  r19.26m  2625  r19.43  2652  rabid2  2671  isset  2766  ralv  2777  rexv  2778  reuv  2779  rmov  2780  rexcom4b  2785  ceqsex4v  2804  ceqsex8v  2806  ceqsrexv  2891  ralrab2  2926  rexrab2  2928  reu2  2949  reu3  2951  reueq  2960  2reuswapdc  2965  reuind  2966  sbc3an  3048  rmo2ilem  3076  csbcow  3092  dfss2  3169  dfss3  3170  dfss3f  3172  ssabral  3251  rabss  3257  ssrabeq  3267  uniiunlem  3269  dfdif3  3270  ddifstab  3292  uncom  3304  inass  3370  indi  3407  difindiss  3414  difin2  3422  reupick3  3445  n0rf  3460  eq0  3466  eqv  3467  vss  3495  disj  3496  disj3  3500  undisj1  3505  undisj2  3506  exsnrex  3661  euabsn2  3688  euabsn  3689  prssg  3776  dfuni2  3838  unissb  3866  elint2  3878  ssint  3887  dfiin2g  3946  iunn0m  3974  iunxun  3993  iunxiun  3995  iinpw  4004  disjnim  4021  dftr2  4130  dftr5  4131  dftr3  4132  dftr4  4133  vnex  4161  inuni  4185  snelpw  4243  sspwb  4246  opelopabsb  4291  eusv2  4489  orddif  4580  onintexmid  4606  zfregfr  4607  tfi  4615  opthprc  4711  elxp3  4714  xpiundir  4719  elvv  4722  brinxp2  4727  relsn  4765  reliun  4781  inxp  4797  raliunxp  4804  rexiunxp  4805  cnvuni  4849  dm0rn0  4880  elrn  4906  ssdmres  4965  dfres2  4995  dfima2  5008  args  5035  cotr  5048  intasym  5051  asymref  5052  intirr  5053  cnv0  5070  xp11m  5105  cnvresima  5156  resco  5171  rnco  5173  coiun  5176  coass  5185  dfiota2  5217  dffun2  5265  dffun6f  5268  dffun4f  5271  dffun7  5282  dffun9  5284  funfn  5285  svrelfun  5320  imadiflem  5334  dffn2  5406  dffn3  5415  fintm  5440  dffn4  5483  dff1o4  5509  brprcneu  5548  eqfnfv3  5658  fnreseql  5669  fsn  5731  abrexco  5803  imaiun  5804  mpo2eqb  6029  elovmpo  6119  abexex  6180  releldm2  6240  fnmpo  6257  dftpos4  6318  tfrlem7  6372  0er  6623  eroveu  6682  erovlem  6683  map0e  6742  elixpconst  6762  domen  6807  reuen1  6857  xpf1o  6902  ssfilem  6933  finexdc  6960  pw1dc0el  6969  ssfirab  6992  sbthlemi10  7027  djuexb  7105  dmaddpq  7441  dmmulpq  7442  distrnqg  7449  enq0enq  7493  enq0tr  7496  nqnq0pi  7500  distrnq0  7521  prltlu  7549  prarloc  7565  genpdflem  7569  ltexprlemm  7662  ltexprlemlol  7664  ltexprlemupu  7666  ltexprlemdisj  7668  recexprlemdisj  7692  ltresr  7901  elnnz  9330  dfz2  9392  2rexuz  9650  eluz2b1  9669  elxr  9845  elixx1  9966  elioo2  9990  elioopnf  10036  elicopnf  10038  elfz1  10082  fzdifsuc  10150  fznn  10158  fzp1nel  10173  fznn0  10182  dfrp2  10335  redivap  11021  imdivap  11028  rexanre  11367  climreu  11443  prodmodc  11724  3dvdsdec  12009  3dvds2dec  12010  bezoutlembi  12145  nnwosdc  12179  isprm2  12258  isprm3  12259  isprm4  12260  pythagtriplem2  12407  elgz  12512  inffinp1  12589  isnsg4  13285  isrng  13433  isring  13499  dfrhm2  13653  lss1d  13882  isbasis3g  14225  restsn  14359  lmbr  14392  txbas  14437  tx2cn  14449  elcncf1di  14758  dedekindicclemicc  14811  limcrcl  14837  bj-nnor  15296  bj-vprc  15458  ss1oel2o  15554  subctctexmid  15561  trirec0xor  15605