Theorem bitr4i 185

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

Syntax hints:   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3bitr2i  206  3bitr2ri  207  3bitr4i  210  3bitr4ri  211  imdistan  433  mpbiran  884  mpbiran2  885  3anrev  932  an6  1255  nfand  1503  19.33b2  1563  nf3  1602  nf4dc  1603  nf4r  1604  equsalh  1658  sb6x  1706  sb5f  1729  sbidm  1776  sb5  1812  sbanv  1814  sborv  1815  sbhb  1861  sb3an  1877  sbel2x  1919  sbal1yz  1922  sbexyz  1924  eu2  1989  2eu4  2038  cleqh  2184  cleqf  2248  dcne  2262  necon3bii  2289  ne3anior  2339  r2alf  2391  r2exf  2392  r19.23t  2475  r19.26-3  2495  r19.26m  2496  r19.43  2521  rabid2  2539  isset  2619  ralv  2630  rexv  2631  reuv  2632  rmov  2633  rexcom4b  2638  ceqsex4v  2656  ceqsex8v  2658  ceqsrexv  2738  ralrab2  2771  rexrab2  2773  reu2  2794  reu3  2796  reueq  2803  2reuswapdc  2808  reuind  2809  sbc3an  2889  rmo2ilem  2917  dfss2  3003  dfss3  3004  dfss3f  3006  ssabral  3081  rabss  3087  ssrabeq  3096  uniiunlem  3098  dfdif3  3099  ddifstab  3121  uncom  3133  inass  3199  indi  3235  difindiss  3242  difin2  3250  reupick3  3273  n0rf  3284  eq0  3290  eqv  3291  vss  3318  disj  3319  disj3  3323  undisj1  3328  undisj2  3329  exsnrex  3468  euabsn2  3494  euabsn  3495  prssg  3577  dfuni2  3638  unissb  3666  elint2  3678  ssint  3687  dfiin2g  3746  iunn0m  3773  iunxun  3791  iunxiun  3792  iinpw  3798  dftr2  3913  dftr5  3914  dftr3  3915  dftr4  3916  vnex  3945  inuni  3966  snelpw  4014  sspwb  4017  opelopabsb  4061  eusv2  4253  orddif  4336  onintexmid  4361  zfregfr  4362  tfi  4370  opthprc  4457  elxp3  4460  xpiundir  4465  elvv  4468  brinxp2  4473  relsn  4511  reliun  4526  inxp  4538  raliunxp  4545  rexiunxp  4546  cnvuni  4590  dm0rn0  4621  elrn  4646  ssdmres  4702  dfres2  4731  dfima2  4743  args  4768  cotr  4780  intasym  4783  asymref  4784  intirr  4785  cnv0  4801  xp11m  4835  cnvresima  4886  resco  4901  rnco  4903  coiun  4906  coass  4915  dfiota2  4947  dffun2  4991  dffun6f  4994  dffun4f  4997  dffun7  5007  dffun9  5009  funfn  5010  svrelfun  5044  imadiflem  5058  dffn2  5128  dffn3  5135  fintm  5159  dffn4  5202  dff1o4  5224  brprcneu  5261  eqfnfv3  5362  fnreseql  5372  fsn  5432  abrexco  5499  imaiun  5500  mpt22eqb  5711  elovmpt2  5802  abexex  5854  releldm2  5912  fnmpt2  5929  dftpos4  5982  tfrlem7  6036  0er  6278  eroveu  6335  erovlem  6336  map0e  6395  domen  6420  reuen1  6470  xpf1o  6512  ssfilem  6543  finexdc  6570  ssfirab  6593  sbthlemi10  6619  dmaddpq  6882  dmmulpq  6883  distrnqg  6890  enq0enq  6934  enq0tr  6937  nqnq0pi  6941  distrnq0  6962  prltlu  6990  prarloc  7006  genpdflem  7010  ltexprlemm  7103  ltexprlemlol  7105  ltexprlemupu  7107  ltexprlemdisj  7109  recexprlemdisj  7133  ltresr  7320  elnnz  8693  dfz2  8752  2rexuz  9002  eluz2b1  9020  elxr  9179  elixx1  9247  elioo2  9271  elioopnf  9317  elicopnf  9319  elfz1  9361  fzdifsuc  9425  fznn  9433  fzp1nel  9448  fznn0  9457  redivap  10204  imdivap  10211  rexanre  10549  climreu  10580  3dvdsdec  10747  3dvds2dec  10748  bezoutlembi  10876  isprm2  10981  isprm3  10982  isprm4  10983  dcdc  11107  bj-vprc  11232  ss1oel2o  11333