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  943  mpbiran2  944  3anrev  991  an6  1334  nfand  1592  19.33b2  1653  nf3  1693  nf4dc  1694  nf4r  1695  equsalh  1750  sb6x  1803  sb5f  1828  sbidm  1875  sb5  1912  sbanv  1914  sborv  1915  sbhb  1969  sb3an  1987  sbel2x  2027  sbal1yz  2030  sbexyz  2032  eu2  2099  2eu4  2148  cleqh  2306  cleqf  2374  dcne  2388  necon3bii  2415  ne3anior  2465  r2alf  2524  r2exf  2525  r19.23t  2614  r19.26-3  2637  r19.26m  2638  r19.43  2665  rabid2  2684  isset  2779  ralv  2790  rexv  2791  reuv  2792  rmov  2793  rexcom4b  2798  ceqsex4v  2817  ceqsex8v  2819  ceqsrexv  2904  ralrab2  2939  rexrab2  2941  reu2  2962  reu3  2964  reueq  2973  2reuswapdc  2978  reuind  2979  sbc3an  3061  rmo2ilem  3089  csbcow  3105  ssalel  3182  dfss3  3183  dfss3f  3186  ssabral  3265  rabss  3271  ssrabeq  3281  uniiunlem  3283  dfdif3  3284  ddifstab  3306  uncom  3318  inass  3384  indi  3421  difindiss  3428  difin2  3436  reupick3  3459  n0rf  3474  eq0  3480  eqv  3481  vss  3509  disj  3510  disj3  3514  undisj1  3519  undisj2  3520  exsnrex  3676  euabsn2  3703  euabsn  3704  snmb  3755  prssg  3792  dfuni2  3854  unissb  3882  elint2  3894  ssint  3903  dfiin2g  3962  iunn0m  3990  iunxun  4009  iunxiun  4011  iinpw  4020  disjnim  4037  dftr2  4148  dftr5  4149  dftr3  4150  dftr4  4151  vnex  4179  inuni  4203  snelpw  4261  sspwb  4264  opelopabsb  4310  eusv2  4508  orddif  4599  onintexmid  4625  zfregfr  4626  tfi  4634  opthprc  4730  elxp3  4733  xpiundir  4738  elvv  4741  brinxp2  4746  relsn  4784  reliun  4800  inxp  4816  raliunxp  4823  rexiunxp  4824  cnvuni  4868  dm0rn0  4900  elrn  4926  ssdmres  4986  dfres2  5016  dfima2  5029  args  5056  cotr  5069  intasym  5072  asymref  5073  intirr  5074  cnv0  5091  xp11m  5126  cnvresima  5177  resco  5192  rnco  5194  coiun  5197  coass  5206  dfiota2  5238  dffun2  5286  dffun6f  5289  dffun4f  5292  dffun7  5303  dffun9  5305  funfn  5306  svrelfun  5344  imadiflem  5358  dffn2  5433  dffn3  5442  fintm  5468  dffn4  5511  dff1o4  5537  brprcneu  5576  eqfnfv3  5686  fnreseql  5697  fsn  5759  abrexco  5835  imaiun  5836  mpo2eqb  6062  elovmpo  6152  abexex  6218  releldm2  6278  fnmpo  6295  dftpos4  6356  tfrlem7  6410  0er  6661  eroveu  6720  erovlem  6721  map0e  6780  elixpconst  6800  domen  6847  reuen1  6900  xpf1o  6948  ssfilem  6979  finexdc  7006  pw1dc0el  7015  ssfirab  7040  sbthlemi10  7075  djuexb  7153  dmaddpq  7499  dmmulpq  7500  distrnqg  7507  enq0enq  7551  enq0tr  7554  nqnq0pi  7558  distrnq0  7579  prltlu  7607  prarloc  7623  genpdflem  7627  ltexprlemm  7720  ltexprlemlol  7722  ltexprlemupu  7724  ltexprlemdisj  7726  recexprlemdisj  7750  ltresr  7959  elnnz  9389  dfz2  9452  2rexuz  9710  eluz2b1  9729  elxr  9905  elixx1  10026  elioo2  10050  elioopnf  10096  elicopnf  10098  elfz1  10142  fzdifsuc  10210  fznn  10218  fzp1nel  10233  fznn0  10242  dfrp2  10413  redivap  11229  imdivap  11236  rexanre  11575  climreu  11652  prodmodc  11933  3dvdsdec  12220  3dvds2dec  12221  bitsval  12298  bezoutlembi  12370  nnwosdc  12404  isprm2  12483  isprm3  12484  isprm4  12485  pythagtriplem2  12633  elgz  12738  inffinp1  12844  isnsg4  13592  isrng  13740  isring  13806  dfrhm2  13960  lss1d  14189  isbasis3g  14562  restsn  14696  lmbr  14729  txbas  14774  tx2cn  14786  elcncf1di  15095  dedekindicclemicc  15148  limcrcl  15174  bj-nnor  15744  bj-vprc  15906  ss1oel2o  16002  subctctexmid  16011  trirec0xor  16058