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  2949  ralrab2  2984  rexrab2  2986  reu2  3007  reu3  3009  reueq  3018  2reuswapdc  3023  reuind  3024  sbc3an  3106  rmo2ilem  3135  csbcow  3151  ssalel  3228  dfss3  3229  dfss3f  3232  ssabral  3311  rabss  3317  ssrabeq  3328  uniiunlem  3330  dfdif3  3331  ddifstab  3353  uncom  3365  inass  3433  indi  3470  difindiss  3477  difin2  3485  reupick3  3508  n0rf  3523  eq0  3529  eqv  3530  vss  3558  disj  3559  disj3  3563  undisj1  3568  undisj2  3569  exsnrex  3733  euabsn2  3762  euabsn  3763  snmb  3815  prssg  3853  dfuni2  3918  unissb  3946  elint2  3958  ssint  3967  dfiin2g  4026  iunn0m  4054  iunxun  4073  iunxiun  4075  iinpw  4084  disjnim  4101  dftr2  4212  dftr5  4213  dftr3  4214  dftr4  4215  vnex  4243  inuni  4269  snelpw  4330  sspwb  4334  opelopabsb  4380  eusv2  4580  orddif  4671  onintexmid  4697  zfregfr  4698  tfi  4706  opthprc  4803  elxp3  4806  xpiundir  4811  elvv  4814  brinxp2  4819  relsn  4857  reliun  4875  inxp  4891  raliunxp  4898  rexiunxp  4899  cnvuni  4943  dm0rn0  4975  elrn  5002  ssdmres  5062  dfres2  5092  dfima2  5105  args  5133  cotr  5146  intasym  5149  asymref  5150  intirr  5151  cnv0  5168  xp11m  5203  cnvresima  5254  resco  5269  rnco  5271  coiun  5274  coass  5283  dfiota2  5315  dffun2  5364  dffun6f  5367  dffun4f  5370  dffun7  5381  dffun9  5383  funfn  5384  svrelfun  5423  imadiflem  5437  dffn2  5512  dffn3  5521  fintm  5554  dffn4  5598  dff1o4  5624  brprcneu  5665  eqfnfv3  5779  fnreseql  5790  fsn  5851  abrexco  5934  imaiun  5935  mpo2eqb  6165  elovmpo  6255  abexex  6321  releldm2  6381  fnmpo  6400  cnvimadfsn  6447  dftpos4  6496  tfrlem7  6550  0er  6803  eroveu  6862  erovlem  6863  map0e  6922  elixpconst  6943  domen  6990  reuen1  7043  xpf1o  7099  ssfilem  7132  ssfilemd  7134  finexdc  7162  pw1dc0el  7173  ssfirab  7199  sbthlemi10  7238  djuexb  7337  sspw1or2  7497  iftrueb01  7535  pw1if  7537  dmaddpq  7699  dmmulpq  7700  distrnqg  7707  enq0enq  7751  enq0tr  7754  nqnq0pi  7758  distrnq0  7779  prltlu  7807  prarloc  7823  genpdflem  7827  ltexprlemm  7920  ltexprlemlol  7922  ltexprlemupu  7924  ltexprlemdisj  7926  recexprlemdisj  7950  ltresr  8159  elnnz  9592  dfz2  9655  2rexuz  9920  eluz2b1  9939  elxr  10115  elixx1  10236  elioo2  10260  elioopnf  10306  elicopnf  10308  elfz1  10353  fzdifsuc  10422  fznn  10430  fzp1nel  10445  fznn0  10454  dfrp2  10630  redivap  11567  imdivap  11574  rexanre  11913  climreu  11990  prodmodc  12272  3dvdsdec  12559  3dvds2dec  12560  bitsval  12637  bezoutlembi  12709  nnwosdc  12743  isprm2  12822  isprm3  12823  isprm4  12824  pythagtriplem2  12972  elgz  13077  inffinp1  13201  isnsg4  13950  isrng  14099  isring  14165  dfrhm2  14321  lss1d  14580  isbasis3g  14960  restsn  15094  lmbr  15127  txbas  15172  tx2cn  15184  elcncf1di  15493  dedekindicclemicc  15546  limcrcl  15572  isclwwlk  16438  clwwlkccatlem  16444  eupth2lem1  16502  bj-nnor  16555  bj-vprc  16715  ss1oel2o  16810  subctctexmid  16823  trirec0xor  16878