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  616  mpbiran  949  mpbiran2  950  3anrev  1015  an6  1358  nfand  1617  19.33b2  1678  nf3  1717  nf4dc  1718  nf4r  1719  equsalh  1774  sb6x  1828  sb5f  1853  sbidm  1900  equsv  1934  sb5  1938  sbanv  1940  sborv  1941  sbhb  1996  sb3an  2014  sbel2x  2054  sbal1yz  2057  sbexyz  2059  eu2  2127  2eu4  2176  cleqh  2334  cleqf  2411  dcne  2425  necon3bii  2452  ne3anior  2502  r2alf  2561  r2exf  2562  r19.23t  2652  r19.26-3  2675  r19.26m  2676  r19.43  2703  rabid2  2723  isset  2822  ralv  2833  rexv  2834  reuv  2835  rmov  2836  rexcom4b  2841  ceqsex4v  2860  ceqsex8v  2862  ceqsrexv  2950  ralrab2  2985  rexrab2  2987  reu2  3008  reu3  3010  reueq  3019  2reuswapdc  3024  reuind  3025  sbc3an  3107  rmo2ilem  3136  csbcow  3152  ssalel  3229  dfss3  3230  dfss3f  3234  ssabral  3313  rabss  3319  ssrabeq  3330  uniiunlem  3332  dfdif3  3333  ddifstab  3355  uncom  3367  inass  3435  indi  3472  difindiss  3479  difin2  3487  reupick3  3510  n0rf  3525  eq0  3531  eqv  3532  vss  3557  disj  3562  disj3  3566  undisj1  3571  undisj2  3572  exsnrex  3737  euabsn2  3766  euabsn  3767  snmb  3819  prssg  3857  dfuni2  3922  unissb  3950  elint2  3962  ssint  3971  dfiin2g  4030  iunn0m  4058  iunxun  4077  iunxiun  4079  iinpw  4088  disjnim  4105  dftr2  4216  dftr5  4217  dftr3  4218  dftr4  4219  vnex  4247  inuni  4273  snelpw  4334  sspwb  4338  opelopabsb  4384  eusv2  4584  orddif  4675  onintexmid  4701  zfregfr  4702  tfi  4710  opthprc  4807  elxp3  4810  xpiundir  4815  elvv  4818  brinxp2  4823  relsn  4861  reliun  4879  inxp  4895  raliunxp  4902  rexiunxp  4903  cnvuni  4947  dm0rn0  4979  elrn  5006  ssdmres  5066  dfres2  5096  dfima2  5109  args  5137  cotr  5150  intasym  5153  asymref  5154  intirr  5155  cnv0  5172  xp11m  5207  cnvresima  5258  resco  5273  rnco  5275  coiun  5278  coass  5287  dfiota2  5319  dffun2  5368  dffun6f  5371  dffun4f  5374  dffun7  5385  dffun9  5387  funfn  5388  svrelfun  5427  imadiflem  5441  dffn2  5516  dffn3  5525  fintm  5558  dffn4  5602  dff1o4  5628  brprcneu  5669  eqfnfv3  5783  fnreseql  5794  fsn  5855  abrexco  5939  imaiun  5940  mpo2eqb  6172  elovmpo  6262  abexex  6329  releldm2  6393  fnmpo  6412  cnvimadfsn  6459  dftpos4  6508  tfrlem7  6562  0er  6815  eroveu  6874  erovlem  6875  map0e  6934  elixpconst  6955  domen  7002  reuen1  7055  xpf1o  7111  ssfilem  7144  ssfilemd  7146  finexdc  7174  pw1dc0el  7185  ssfirab  7211  sbthlemi10  7250  djuexb  7349  sspw1or2  7509  iftrueb01  7547  pw1if  7549  dmaddpq  7711  dmmulpq  7712  distrnqg  7719  enq0enq  7763  enq0tr  7766  nqnq0pi  7770  distrnq0  7791  prltlu  7819  prarloc  7835  genpdflem  7839  ltexprlemm  7932  ltexprlemlol  7934  ltexprlemupu  7936  ltexprlemdisj  7938  recexprlemdisj  7962  ltresr  8171  elnnz  9608  dfz2  9671  2rexuz  9936  eluz2b1  9955  elxr  10132  elixx1  10253  elioo2  10277  elioopnf  10323  elicopnf  10325  elfz1  10370  fzdifsuc  10441  fznn  10449  fzp1nel  10464  fznn0  10473  dfrp2  10651  redivap  11588  imdivap  11595  rexanre  11935  climreu  12012  prodmodc  12294  3dvdsdec  12581  3dvds2dec  12582  bitsval  12659  bezoutlembi  12731  nnwosdc  12765  isprm2  12844  isprm3  12845  isprm4  12846  pythagtriplem2  12994  elgz  13099  inffinp1  13269  isnsg4  13970  isrng  14178  isring  14248  dfrhm2  14404  lss1d  14662  isbasis3g  15042  restsn  15176  lmbr  15209  txbas  15254  tx2cn  15266  elcncf1di  15575  dedekindicclemicc  15628  limcrcl  15654  isclwwlk  16520  clwwlkccatlem  16526  eupth2lem1  16584  bj-nnor  16647  bj-vprc  16807  ss1oel2o  16902  subctctexmid  16915  trirec0xor  16970