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  442  bianass  466  biadani  607  mpbiran  935  mpbiran2  936  3anrev  983  an6  1316  nfand  1561  19.33b2  1622  nf3  1662  nf4dc  1663  nf4r  1664  equsalh  1719  sb6x  1772  sb5f  1797  sbidm  1844  sb5  1880  sbanv  1882  sborv  1883  sbhb  1933  sb3an  1951  sbel2x  1991  sbal1yz  1994  sbexyz  1996  eu2  2063  2eu4  2112  cleqh  2270  cleqf  2337  dcne  2351  necon3bii  2378  ne3anior  2428  r2alf  2487  r2exf  2488  r19.23t  2577  r19.26-3  2600  r19.26m  2601  r19.43  2628  rabid2  2646  isset  2736  ralv  2747  rexv  2748  reuv  2749  rmov  2750  rexcom4b  2755  ceqsex4v  2773  ceqsex8v  2775  ceqsrexv  2860  ralrab2  2895  rexrab2  2897  reu2  2918  reu3  2920  reueq  2929  2reuswapdc  2934  reuind  2935  sbc3an  3016  rmo2ilem  3044  csbcow  3060  dfss2  3136  dfss3  3137  dfss3f  3139  ssabral  3218  rabss  3224  ssrabeq  3234  uniiunlem  3236  dfdif3  3237  ddifstab  3259  uncom  3271  inass  3337  indi  3374  difindiss  3381  difin2  3389  reupick3  3412  n0rf  3427  eq0  3433  eqv  3434  vss  3462  disj  3463  disj3  3467  undisj1  3472  undisj2  3473  exsnrex  3625  euabsn2  3652  euabsn  3653  prssg  3737  dfuni2  3798  unissb  3826  elint2  3838  ssint  3847  dfiin2g  3906  iunn0m  3933  iunxun  3952  iunxiun  3954  iinpw  3963  disjnim  3980  dftr2  4089  dftr5  4090  dftr3  4091  dftr4  4092  vnex  4120  inuni  4141  snelpw  4198  sspwb  4201  opelopabsb  4245  eusv2  4442  orddif  4531  onintexmid  4557  zfregfr  4558  tfi  4566  opthprc  4662  elxp3  4665  xpiundir  4670  elvv  4673  brinxp2  4678  relsn  4716  reliun  4732  inxp  4745  raliunxp  4752  rexiunxp  4753  cnvuni  4797  dm0rn0  4828  elrn  4854  ssdmres  4913  dfres2  4943  dfima2  4955  args  4980  cotr  4992  intasym  4995  asymref  4996  intirr  4997  cnv0  5014  xp11m  5049  cnvresima  5100  resco  5115  rnco  5117  coiun  5120  coass  5129  dfiota2  5161  dffun2  5208  dffun6f  5211  dffun4f  5214  dffun7  5225  dffun9  5227  funfn  5228  svrelfun  5263  imadiflem  5277  dffn2  5349  dffn3  5358  fintm  5383  dffn4  5426  dff1o4  5450  brprcneu  5489  eqfnfv3  5595  fnreseql  5606  fsn  5668  abrexco  5738  imaiun  5739  mpo2eqb  5962  elovmpo  6050  abexex  6105  releldm2  6164  fnmpo  6181  dftpos4  6242  tfrlem7  6296  0er  6547  eroveu  6604  erovlem  6605  map0e  6664  elixpconst  6684  domen  6729  reuen1  6779  xpf1o  6822  ssfilem  6853  finexdc  6880  pw1dc0el  6889  ssfirab  6911  sbthlemi10  6943  djuexb  7021  dmaddpq  7341  dmmulpq  7342  distrnqg  7349  enq0enq  7393  enq0tr  7396  nqnq0pi  7400  distrnq0  7421  prltlu  7449  prarloc  7465  genpdflem  7469  ltexprlemm  7562  ltexprlemlol  7564  ltexprlemupu  7566  ltexprlemdisj  7568  recexprlemdisj  7592  ltresr  7801  elnnz  9222  dfz2  9284  2rexuz  9541  eluz2b1  9560  elxr  9733  elixx1  9854  elioo2  9878  elioopnf  9924  elicopnf  9926  elfz1  9970  fzdifsuc  10037  fznn  10045  fzp1nel  10060  fznn0  10069  dfrp2  10220  redivap  10838  imdivap  10845  rexanre  11184  climreu  11260  prodmodc  11541  3dvdsdec  11824  3dvds2dec  11825  bezoutlembi  11960  nnwosdc  11994  isprm2  12071  isprm3  12072  isprm4  12073  pythagtriplem2  12220  elgz  12323  inffinp1  12384  isbasis3g  12838  restsn  12974  lmbr  13007  txbas  13052  tx2cn  13064  elcncf1di  13360  dedekindicclemicc  13404  limcrcl  13421  bj-nnor  13769  bj-vprc  13931  ss1oel2o  14026  subctctexmid  14034  trirec0xor  14077