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  1582  19.33b2  1643  nf3  1683  nf4dc  1684  nf4r  1685  equsalh  1740  sb6x  1793  sb5f  1818  sbidm  1865  sb5  1902  sbanv  1904  sborv  1905  sbhb  1959  sb3an  1977  sbel2x  2017  sbal1yz  2020  sbexyz  2022  eu2  2089  2eu4  2138  cleqh  2296  cleqf  2364  dcne  2378  necon3bii  2405  ne3anior  2455  r2alf  2514  r2exf  2515  r19.23t  2604  r19.26-3  2627  r19.26m  2628  r19.43  2655  rabid2  2674  isset  2769  ralv  2780  rexv  2781  reuv  2782  rmov  2783  rexcom4b  2788  ceqsex4v  2807  ceqsex8v  2809  ceqsrexv  2894  ralrab2  2929  rexrab2  2931  reu2  2952  reu3  2954  reueq  2963  2reuswapdc  2968  reuind  2969  sbc3an  3051  rmo2ilem  3079  csbcow  3095  ssalel  3172  dfss3  3173  dfss3f  3176  ssabral  3255  rabss  3261  ssrabeq  3271  uniiunlem  3273  dfdif3  3274  ddifstab  3296  uncom  3308  inass  3374  indi  3411  difindiss  3418  difin2  3426  reupick3  3449  n0rf  3464  eq0  3470  eqv  3471  vss  3499  disj  3500  disj3  3504  undisj1  3509  undisj2  3510  exsnrex  3665  euabsn2  3692  euabsn  3693  prssg  3780  dfuni2  3842  unissb  3870  elint2  3882  ssint  3891  dfiin2g  3950  iunn0m  3978  iunxun  3997  iunxiun  3999  iinpw  4008  disjnim  4025  dftr2  4134  dftr5  4135  dftr3  4136  dftr4  4137  vnex  4165  inuni  4189  snelpw  4247  sspwb  4250  opelopabsb  4295  eusv2  4493  orddif  4584  onintexmid  4610  zfregfr  4611  tfi  4619  opthprc  4715  elxp3  4718  xpiundir  4723  elvv  4726  brinxp2  4731  relsn  4769  reliun  4785  inxp  4801  raliunxp  4808  rexiunxp  4809  cnvuni  4853  dm0rn0  4884  elrn  4910  ssdmres  4969  dfres2  4999  dfima2  5012  args  5039  cotr  5052  intasym  5055  asymref  5056  intirr  5057  cnv0  5074  xp11m  5109  cnvresima  5160  resco  5175  rnco  5177  coiun  5180  coass  5189  dfiota2  5221  dffun2  5269  dffun6f  5272  dffun4f  5275  dffun7  5286  dffun9  5288  funfn  5289  svrelfun  5324  imadiflem  5338  dffn2  5412  dffn3  5421  fintm  5446  dffn4  5489  dff1o4  5515  brprcneu  5554  eqfnfv3  5664  fnreseql  5675  fsn  5737  abrexco  5809  imaiun  5810  mpo2eqb  6036  elovmpo  6126  abexex  6192  releldm2  6252  fnmpo  6269  dftpos4  6330  tfrlem7  6384  0er  6635  eroveu  6694  erovlem  6695  map0e  6754  elixpconst  6774  domen  6819  reuen1  6869  xpf1o  6914  ssfilem  6945  finexdc  6972  pw1dc0el  6981  ssfirab  7006  sbthlemi10  7041  djuexb  7119  dmaddpq  7465  dmmulpq  7466  distrnqg  7473  enq0enq  7517  enq0tr  7520  nqnq0pi  7524  distrnq0  7545  prltlu  7573  prarloc  7589  genpdflem  7593  ltexprlemm  7686  ltexprlemlol  7688  ltexprlemupu  7690  ltexprlemdisj  7692  recexprlemdisj  7716  ltresr  7925  elnnz  9355  dfz2  9417  2rexuz  9675  eluz2b1  9694  elxr  9870  elixx1  9991  elioo2  10015  elioopnf  10061  elicopnf  10063  elfz1  10107  fzdifsuc  10175  fznn  10183  fzp1nel  10198  fznn0  10207  dfrp2  10372  redivap  11058  imdivap  11065  rexanre  11404  climreu  11481  prodmodc  11762  3dvdsdec  12049  3dvds2dec  12050  bitsval  12127  bezoutlembi  12199  nnwosdc  12233  isprm2  12312  isprm3  12313  isprm4  12314  pythagtriplem2  12462  elgz  12567  inffinp1  12673  isnsg4  13420  isrng  13568  isring  13634  dfrhm2  13788  lss1d  14017  isbasis3g  14368  restsn  14502  lmbr  14535  txbas  14580  tx2cn  14592  elcncf1di  14901  dedekindicclemicc  14954  limcrcl  14980  bj-nnor  15466  bj-vprc  15628  ss1oel2o  15724  subctctexmid  15733  trirec0xor  15780