Theorem bitr4i 186

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 131	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	bitri 183	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitr2i  207  3bitr2ri  208  3bitr4i  211  3bitr4ri  212  biancomi  268  imdistan  440  biadani  601  mpbiran  924  mpbiran2  925  3anrev  972  an6  1299  nfand  1547  19.33b2  1608  nf3  1647  nf4dc  1648  nf4r  1649  equsalh  1704  sb6x  1752  sb5f  1776  sbidm  1823  sb5  1859  sbanv  1861  sborv  1862  sbhb  1913  sb3an  1931  sbel2x  1973  sbal1yz  1976  sbexyz  1978  eu2  2043  2eu4  2092  cleqh  2239  cleqf  2305  dcne  2319  necon3bii  2346  ne3anior  2396  r2alf  2452  r2exf  2453  r19.23t  2539  r19.26-3  2562  r19.26m  2563  r19.43  2589  rabid2  2607  isset  2692  ralv  2703  rexv  2704  reuv  2705  rmov  2706  rexcom4b  2711  ceqsex4v  2729  ceqsex8v  2731  ceqsrexv  2815  ralrab2  2849  rexrab2  2851  reu2  2872  reu3  2874  reueq  2883  2reuswapdc  2888  reuind  2889  sbc3an  2970  rmo2ilem  2998  dfss2  3086  dfss3  3087  dfss3f  3089  ssabral  3168  rabss  3174  ssrabeq  3183  uniiunlem  3185  dfdif3  3186  ddifstab  3208  uncom  3220  inass  3286  indi  3323  difindiss  3330  difin2  3338  reupick3  3361  n0rf  3375  eq0  3381  eqv  3382  vss  3410  disj  3411  disj3  3415  undisj1  3420  undisj2  3421  exsnrex  3566  euabsn2  3592  euabsn  3593  prssg  3677  dfuni2  3738  unissb  3766  elint2  3778  ssint  3787  dfiin2g  3846  iunn0m  3873  iunxun  3892  iunxiun  3894  iinpw  3903  disjnim  3920  dftr2  4028  dftr5  4029  dftr3  4030  dftr4  4031  vnex  4059  inuni  4080  snelpw  4135  sspwb  4138  opelopabsb  4182  eusv2  4378  orddif  4462  onintexmid  4487  zfregfr  4488  tfi  4496  opthprc  4590  elxp3  4593  xpiundir  4598  elvv  4601  brinxp2  4606  relsn  4644  reliun  4660  inxp  4673  raliunxp  4680  rexiunxp  4681  cnvuni  4725  dm0rn0  4756  elrn  4782  ssdmres  4841  dfres2  4871  dfima2  4883  args  4908  cotr  4920  intasym  4923  asymref  4924  intirr  4925  cnv0  4942  xp11m  4977  cnvresima  5028  resco  5043  rnco  5045  coiun  5048  coass  5057  dfiota2  5089  dffun2  5133  dffun6f  5136  dffun4f  5139  dffun7  5150  dffun9  5152  funfn  5153  svrelfun  5188  imadiflem  5202  dffn2  5274  dffn3  5283  fintm  5308  dffn4  5351  dff1o4  5375  brprcneu  5414  eqfnfv3  5520  fnreseql  5530  fsn  5592  abrexco  5660  imaiun  5661  mpo2eqb  5880  elovmpo  5971  abexex  6024  releldm2  6083  fnmpo  6100  dftpos4  6160  tfrlem7  6214  0er  6463  eroveu  6520  erovlem  6521  map0e  6580  elixpconst  6600  domen  6645  reuen1  6695  xpf1o  6738  ssfilem  6769  finexdc  6796  ssfirab  6822  sbthlemi10  6854  djuexb  6929  dmaddpq  7187  dmmulpq  7188  distrnqg  7195  enq0enq  7239  enq0tr  7242  nqnq0pi  7246  distrnq0  7267  prltlu  7295  prarloc  7311  genpdflem  7315  ltexprlemm  7408  ltexprlemlol  7410  ltexprlemupu  7412  ltexprlemdisj  7414  recexprlemdisj  7438  ltresr  7647  elnnz  9064  dfz2  9123  2rexuz  9377  eluz2b1  9395  elxr  9563  elixx1  9680  elioo2  9704  elioopnf  9750  elicopnf  9752  elfz1  9795  fzdifsuc  9861  fznn  9869  fzp1nel  9884  fznn0  9893  redivap  10646  imdivap  10653  rexanre  10992  climreu  11066  prodmodc  11347  3dvdsdec  11562  3dvds2dec  11563  bezoutlembi  11693  isprm2  11798  isprm3  11799  isprm4  11800  inffinp1  11942  isbasis3g  12213  restsn  12349  lmbr  12382  txbas  12427  tx2cn  12439  elcncf1di  12735  dedekindicclemicc  12779  limcrcl  12796  bj-nnor  12946  bj-vprc  13094  ss1oel2o  13189  subctctexmid  13196