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 ⊢ (𝜑 ↔ 𝜒)

This proof depends on syntax axioms:   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3bitr2i  208  3bitr2ri  209  3bitr4i  212  3bitr4ri  213  biancomi  270  imdistan  448  bianass  473  biadani  620  mpbiran  953  mpbiran2  954  3anrev  1019  an6  1362  nfand  1621  19.33b2  1682  nf3  1721  nf4dc  1722  nf4r  1723  equsalh  1778  sb6x  1832  sb5f  1857  sbidm  1904  equsv  1938  sb5  1942  sbanv  1944  sborv  1945  sbhb  2000  sb3an  2018  sbel2x  2058  sbal1yz  2061  sbexyz  2063  eu2  2131  2eu4  2180  cleqh  2338  cleqf  2417  dcne  2431  necon3bii  2458  ne3anior  2508  r2alf  2567  r2exf  2568  r19.23t  2658  r19.26-3  2681  r19.26m  2682  r19.43  2709  rabid2  2729  isset  2828  ralv  2839  rexv  2840  reuv  2841  rmov  2842  rexcom4b  2847  ceqsex4v  2866  ceqsex8v  2868  ceqsrexv  2956  ralrab2  2991  rexrab2  2993  reu2  3014  reu3  3016  reueq  3025  2reuswapdc  3030  reuind  3031  sbc3an  3113  rmo2ilem  3142  csbcow  3158  ssalel  3235  dfss3  3236  dfss3f  3240  ssabral  3319  rabss  3325  ssrabeq  3336  uniiunlem  3338  dfdif3  3339  ddifstab  3361  uncom  3373  inass  3441  indi  3478  difindiss  3485  difin2  3493  reupick3  3518  n0rf  3534  eq0  3540  eqv  3541  vss  3568  disj  3573  disj3  3577  undisj1  3582  undisj2  3583  exsnrex  3751  euabsn2  3780  euabsn  3781  snmb  3834  prssg  3872  dfuni2  3937  unissb  3965  elint2  3977  ssint  3986  dfiin2g  4045  iunn0m  4073  iunxun  4092  iunxiun  4094  iinpw  4103  disjnim  4120  dftr2  4233  dftr5  4234  dftr3  4235  dftr4  4236  vnex  4266  inuni  4293  snelpw  4354  sspwb  4358  opelopabsb  4404  eusv2  4605  orddif  4696  onintexmid  4722  zfregfr  4723  tfi  4731  opthprc  4828  elxp3  4831  xpiundir  4836  elvv  4839  brinxp2  4844  relsn  4882  reliun  4900  inxp  4916  raliunxp  4923  rexiunxp  4924  cnvuni  4968  dm0rn0  5000  elrn  5027  ssdmres  5087  dfres2  5118  dfima2  5131  args  5159  cotr  5172  intasym  5175  asymref  5176  intirr  5177  cnv0  5194  xp11m  5229  cnvresima  5280  resco  5295  rnco  5297  coiun  5300  coass  5309  dfiota2  5341  dffun2  5390  dffun6f  5393  dffun4f  5396  dffun7  5407  dffun9  5409  funfn  5410  svrelfun  5449  imadiflem  5463  dffn2  5538  dffn3  5547  fintm  5580  dffn4  5624  dff1o4  5650  brprcneu  5691  eqfnfv3  5811  fnreseql  5822  fsn  5883  abrexco  5968  imaiun  5969  mpo2eqb  6201  elovmpo  6291  abexex  6359  releldm2  6423  fnmpo  6442  cnvimadfsn  6489  dftpos4  6538  tfrlem7  6592  0er  6845  eroveu  6904  erovlem  6905  map0e  6971  elixpconst  6993  domen  7040  reuen1  7093  xpf1o  7149  ssfilem  7182  ssfilemd  7184  finexdc  7212  pw1dc0el  7223  ssfirab  7249  sbthlemi10  7289  djuexb  7391  sspw1or2  7551  iftrueb01  7589  pw1if  7591  dmaddpq  7753  dmmulpq  7754  distrnqg  7761  enq0enq  7805  enq0tr  7808  nqnq0pi  7812  distrnq0  7833  prltlu  7861  prarloc  7877  genpdflem  7881  ltexprlemm  7974  ltexprlemlol  7976  ltexprlemupu  7978  ltexprlemdisj  7980  recexprlemdisj  8004  ltresr  8213  elnnz  9666  dfz2  9729  2rexuz  9999  eluz2b1  10018  elxr  10196  elixx1  10317  elioo2  10341  elioopnf  10387  elicopnf  10389  elfz1  10434  fzdifsuc  10506  fznn  10514  fzp1nel  10529  fznn0  10538  dfrp2  10716  hashf1  11310  redivap  11662  imdivap  11669  rexanre  12010  climreu  12089  prodmodc  12371  3dvdsdec  12658  3dvds2dec  12659  bitsval  12736  bezoutlembi  12808  nnwosdc  12842  isprm2  12921  isprm3  12922  isprm4  12923  pythagtriplem2  13075  elgz  13180  inffinp1  13379  isnsg4  14075  isrng  14341  isring  14412  dfrhm2  14571  lss1d  14830  isbasis3g  15284  restsn  15418  lmbr  15451  txbas  15496  tx2cn  15508  elcncf1di  15817  dedekindicclemicc  15870  limcrcl  15896  isclwwlk  16852  clwwlkccatlem  16858  eupth2lem1  16916  bj-nnor  16979  bj-vprc  17139  ss1oel2o  17234  subctctexmid  17247  trirec0xor  17313  dfrals2  17349  dfralseu2  17383