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-1 5  ax-2 6  ax-mp 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  imdistan  436  biadani  582  mpbiran  892  mpbiran2  893  3anrev  940  an6  1267  nfand  1515  19.33b2  1576  nf3  1615  nf4dc  1616  nf4r  1617  equsalh  1672  sb6x  1720  sb5f  1743  sbidm  1790  sb5  1826  sbanv  1828  sborv  1829  sbhb  1876  sb3an  1892  sbel2x  1934  sbal1yz  1937  sbexyz  1939  eu2  2004  2eu4  2053  cleqh  2199  cleqf  2264  dcne  2278  necon3bii  2305  ne3anior  2355  r2alf  2411  r2exf  2412  r19.23t  2498  r19.26-3  2521  r19.26m  2522  r19.43  2547  rabid2  2565  isset  2647  ralv  2658  rexv  2659  reuv  2660  rmov  2661  rexcom4b  2666  ceqsex4v  2684  ceqsex8v  2686  ceqsrexv  2769  ralrab2  2802  rexrab2  2804  reu2  2825  reu3  2827  reueq  2836  2reuswapdc  2841  reuind  2842  sbc3an  2922  rmo2ilem  2950  dfss2  3036  dfss3  3037  dfss3f  3039  ssabral  3115  rabss  3121  ssrabeq  3130  uniiunlem  3132  dfdif3  3133  ddifstab  3155  uncom  3167  inass  3233  indi  3270  difindiss  3277  difin2  3285  reupick3  3308  n0rf  3322  eq0  3328  eqv  3329  vss  3357  disj  3358  disj3  3362  undisj1  3367  undisj2  3368  exsnrex  3513  euabsn2  3539  euabsn  3540  prssg  3624  dfuni2  3685  unissb  3713  elint2  3725  ssint  3734  dfiin2g  3793  iunn0m  3820  iunxun  3839  iunxiun  3840  iinpw  3849  disjnim  3866  dftr2  3968  dftr5  3969  dftr3  3970  dftr4  3971  vnex  3999  inuni  4020  snelpw  4073  sspwb  4076  opelopabsb  4120  eusv2  4316  orddif  4400  onintexmid  4425  zfregfr  4426  tfi  4434  opthprc  4528  elxp3  4531  xpiundir  4536  elvv  4539  brinxp2  4544  relsn  4582  reliun  4598  inxp  4611  raliunxp  4618  rexiunxp  4619  cnvuni  4663  dm0rn0  4694  elrn  4720  ssdmres  4777  dfres2  4807  dfima2  4819  args  4844  cotr  4856  intasym  4859  asymref  4860  intirr  4861  cnv0  4878  xp11m  4913  cnvresima  4964  resco  4979  rnco  4981  coiun  4984  coass  4993  dfiota2  5025  dffun2  5069  dffun6f  5072  dffun4f  5075  dffun7  5086  dffun9  5088  funfn  5089  svrelfun  5124  imadiflem  5138  dffn2  5210  dffn3  5219  fintm  5244  dffn4  5287  dff1o4  5309  brprcneu  5346  eqfnfv3  5452  fnreseql  5462  fsn  5524  abrexco  5592  imaiun  5593  mpo2eqb  5812  elovmpo  5903  abexex  5955  releldm2  6013  fnmpo  6030  dftpos4  6090  tfrlem7  6144  0er  6393  eroveu  6450  erovlem  6451  map0e  6510  elixpconst  6530  domen  6575  reuen1  6625  xpf1o  6667  ssfilem  6698  finexdc  6725  ssfirab  6750  sbthlemi10  6782  djuexb  6844  dmaddpq  7088  dmmulpq  7089  distrnqg  7096  enq0enq  7140  enq0tr  7143  nqnq0pi  7147  distrnq0  7168  prltlu  7196  prarloc  7212  genpdflem  7216  ltexprlemm  7309  ltexprlemlol  7311  ltexprlemupu  7313  ltexprlemdisj  7315  recexprlemdisj  7339  ltresr  7526  elnnz  8916  dfz2  8975  2rexuz  9227  eluz2b1  9245  elxr  9404  elixx1  9521  elioo2  9545  elioopnf  9591  elicopnf  9593  elfz1  9636  fzdifsuc  9702  fznn  9710  fzp1nel  9725  fznn0  9734  redivap  10487  imdivap  10494  rexanre  10832  climreu  10905  3dvdsdec  11357  3dvds2dec  11358  bezoutlembi  11486  isprm2  11591  isprm3  11592  isprm4  11593  inffinp1  11734  isbasis3g  11995  restsn  12131  lmbr  12163  txbas  12208  tx2cn  12220  elcncf1di  12479  limcrcl  12509  dcdc  12550  bj-vprc  12675  ss1oel2o  12774