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  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  3750  euabsn2  3779  euabsn  3780  snmb  3832  prssg  3870  dfuni2  3935  unissb  3963  elint2  3975  ssint  3984  dfiin2g  4043  iunn0m  4071  iunxun  4090  iunxiun  4092  iinpw  4101  disjnim  4118  dftr2  4229  dftr5  4230  dftr3  4231  dftr4  4232  vnex  4262  inuni  4289  snelpw  4350  sspwb  4354  opelopabsb  4400  eusv2  4601  orddif  4692  onintexmid  4718  zfregfr  4719  tfi  4727  opthprc  4824  elxp3  4827  xpiundir  4832  elvv  4835  brinxp2  4840  relsn  4878  reliun  4896  inxp  4912  raliunxp  4919  rexiunxp  4920  cnvuni  4964  dm0rn0  4996  elrn  5023  ssdmres  5083  dfres2  5113  dfima2  5126  args  5154  cotr  5167  intasym  5170  asymref  5171  intirr  5172  cnv0  5189  xp11m  5224  cnvresima  5275  resco  5290  rnco  5292  coiun  5295  coass  5304  dfiota2  5336  dffun2  5385  dffun6f  5388  dffun4f  5391  dffun7  5402  dffun9  5404  funfn  5405  svrelfun  5444  imadiflem  5458  dffn2  5533  dffn3  5542  fintm  5575  dffn4  5619  dff1o4  5645  brprcneu  5686  eqfnfv3  5802  fnreseql  5813  fsn  5874  abrexco  5959  imaiun  5960  mpo2eqb  6192  elovmpo  6282  abexex  6349  releldm2  6413  fnmpo  6432  cnvimadfsn  6479  dftpos4  6528  tfrlem7  6582  0er  6835  eroveu  6894  erovlem  6895  map0e  6961  elixpconst  6982  domen  7029  reuen1  7082  xpf1o  7138  ssfilem  7171  ssfilemd  7173  finexdc  7201  pw1dc0el  7212  ssfirab  7238  sbthlemi10  7277  djuexb  7378  sspw1or2  7538  iftrueb01  7576  pw1if  7578  dmaddpq  7740  dmmulpq  7741  distrnqg  7748  enq0enq  7792  enq0tr  7795  nqnq0pi  7799  distrnq0  7820  prltlu  7848  prarloc  7864  genpdflem  7868  ltexprlemm  7961  ltexprlemlol  7963  ltexprlemupu  7965  ltexprlemdisj  7967  recexprlemdisj  7991  ltresr  8200  elnnz  9637  dfz2  9700  2rexuz  9965  eluz2b1  9984  elxr  10161  elixx1  10282  elioo2  10306  elioopnf  10352  elicopnf  10354  elfz1  10399  fzdifsuc  10471  fznn  10479  fzp1nel  10494  fznn0  10503  dfrp2  10681  hashf1  11270  redivap  11622  imdivap  11629  rexanre  11969  climreu  12046  prodmodc  12328  3dvdsdec  12615  3dvds2dec  12616  bitsval  12693  bezoutlembi  12765  nnwosdc  12799  isprm2  12878  isprm3  12879  isprm4  12880  pythagtriplem2  13028  elgz  13133  inffinp1  13303  isnsg4  13998  isrng  14216  isring  14287  dfrhm2  14444  lss1d  14703  isbasis3g  15130  restsn  15264  lmbr  15297  txbas  15342  tx2cn  15354  elcncf1di  15663  dedekindicclemicc  15716  limcrcl  15742  isclwwlk  16618  clwwlkccatlem  16624  eupth2lem1  16682  bj-nnor  16745  bj-vprc  16905  ss1oel2o  17000  subctctexmid  17013  trirec0xor  17068  dfrals2  17104