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  441  biadani  602  mpbiran  930  mpbiran2  931  3anrev  978  an6  1311  nfand  1556  19.33b2  1617  nf3  1657  nf4dc  1658  nf4r  1659  equsalh  1714  sb6x  1767  sb5f  1792  sbidm  1839  sb5  1875  sbanv  1877  sborv  1878  sbhb  1928  sb3an  1946  sbel2x  1986  sbal1yz  1989  sbexyz  1991  eu2  2058  2eu4  2107  cleqh  2266  cleqf  2333  dcne  2347  necon3bii  2374  ne3anior  2424  r2alf  2483  r2exf  2484  r19.23t  2573  r19.26-3  2596  r19.26m  2597  r19.43  2624  rabid2  2642  isset  2732  ralv  2743  rexv  2744  reuv  2745  rmov  2746  rexcom4b  2751  ceqsex4v  2769  ceqsex8v  2771  ceqsrexv  2856  ralrab2  2891  rexrab2  2893  reu2  2914  reu3  2916  reueq  2925  2reuswapdc  2930  reuind  2931  sbc3an  3012  rmo2ilem  3040  csbcow  3056  dfss2  3131  dfss3  3132  dfss3f  3134  ssabral  3213  rabss  3219  ssrabeq  3229  uniiunlem  3231  dfdif3  3232  ddifstab  3254  uncom  3266  inass  3332  indi  3369  difindiss  3376  difin2  3384  reupick3  3407  n0rf  3421  eq0  3427  eqv  3428  vss  3456  disj  3457  disj3  3461  undisj1  3466  undisj2  3467  exsnrex  3618  euabsn2  3645  euabsn  3646  prssg  3730  dfuni2  3791  unissb  3819  elint2  3831  ssint  3840  dfiin2g  3899  iunn0m  3926  iunxun  3945  iunxiun  3947  iinpw  3956  disjnim  3973  dftr2  4082  dftr5  4083  dftr3  4084  dftr4  4085  vnex  4113  inuni  4134  snelpw  4191  sspwb  4194  opelopabsb  4238  eusv2  4435  orddif  4524  onintexmid  4550  zfregfr  4551  tfi  4559  opthprc  4655  elxp3  4658  xpiundir  4663  elvv  4666  brinxp2  4671  relsn  4709  reliun  4725  inxp  4738  raliunxp  4745  rexiunxp  4746  cnvuni  4790  dm0rn0  4821  elrn  4847  ssdmres  4906  dfres2  4936  dfima2  4948  args  4973  cotr  4985  intasym  4988  asymref  4989  intirr  4990  cnv0  5007  xp11m  5042  cnvresima  5093  resco  5108  rnco  5110  coiun  5113  coass  5122  dfiota2  5154  dffun2  5198  dffun6f  5201  dffun4f  5204  dffun7  5215  dffun9  5217  funfn  5218  svrelfun  5253  imadiflem  5267  dffn2  5339  dffn3  5348  fintm  5373  dffn4  5416  dff1o4  5440  brprcneu  5479  eqfnfv3  5585  fnreseql  5595  fsn  5657  abrexco  5727  imaiun  5728  mpo2eqb  5951  elovmpo  6039  abexex  6094  releldm2  6153  fnmpo  6170  dftpos4  6231  tfrlem7  6285  0er  6535  eroveu  6592  erovlem  6593  map0e  6652  elixpconst  6672  domen  6717  reuen1  6767  xpf1o  6810  ssfilem  6841  finexdc  6868  pw1dc0el  6877  ssfirab  6899  sbthlemi10  6931  djuexb  7009  dmaddpq  7320  dmmulpq  7321  distrnqg  7328  enq0enq  7372  enq0tr  7375  nqnq0pi  7379  distrnq0  7400  prltlu  7428  prarloc  7444  genpdflem  7448  ltexprlemm  7541  ltexprlemlol  7543  ltexprlemupu  7545  ltexprlemdisj  7547  recexprlemdisj  7571  ltresr  7780  elnnz  9201  dfz2  9263  2rexuz  9520  eluz2b1  9539  elxr  9712  elixx1  9833  elioo2  9857  elioopnf  9903  elicopnf  9905  elfz1  9949  fzdifsuc  10016  fznn  10024  fzp1nel  10039  fznn0  10048  dfrp2  10199  redivap  10816  imdivap  10823  rexanre  11162  climreu  11238  prodmodc  11519  3dvdsdec  11802  3dvds2dec  11803  bezoutlembi  11938  nnwosdc  11972  isprm2  12049  isprm3  12050  isprm4  12051  pythagtriplem2  12198  elgz  12301  inffinp1  12362  isbasis3g  12684  restsn  12820  lmbr  12853  txbas  12898  tx2cn  12910  elcncf1di  13206  dedekindicclemicc  13250  limcrcl  13267  bj-nnor  13615  bj-vprc  13778  ss1oel2o  13873  subctctexmid  13881  trirec0xor  13924