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  612  mpbiran  942  mpbiran2  943  3anrev  990  an6  1332  nfand  1579  19.33b2  1640  nf3  1680  nf4dc  1681  nf4r  1682  equsalh  1737  sb6x  1790  sb5f  1815  sbidm  1862  sb5  1899  sbanv  1901  sborv  1902  sbhb  1952  sb3an  1970  sbel2x  2010  sbal1yz  2013  sbexyz  2015  eu2  2082  2eu4  2131  cleqh  2289  cleqf  2357  dcne  2371  necon3bii  2398  ne3anior  2448  r2alf  2507  r2exf  2508  r19.23t  2597  r19.26-3  2620  r19.26m  2621  r19.43  2648  rabid2  2667  isset  2758  ralv  2769  rexv  2770  reuv  2771  rmov  2772  rexcom4b  2777  ceqsex4v  2795  ceqsex8v  2797  ceqsrexv  2882  ralrab2  2917  rexrab2  2919  reu2  2940  reu3  2942  reueq  2951  2reuswapdc  2956  reuind  2957  sbc3an  3039  rmo2ilem  3067  csbcow  3083  dfss2  3159  dfss3  3160  dfss3f  3162  ssabral  3241  rabss  3247  ssrabeq  3257  uniiunlem  3259  dfdif3  3260  ddifstab  3282  uncom  3294  inass  3360  indi  3397  difindiss  3404  difin2  3412  reupick3  3435  n0rf  3450  eq0  3456  eqv  3457  vss  3485  disj  3486  disj3  3490  undisj1  3495  undisj2  3496  exsnrex  3649  euabsn2  3676  euabsn  3677  prssg  3764  dfuni2  3826  unissb  3854  elint2  3866  ssint  3875  dfiin2g  3934  iunn0m  3962  iunxun  3981  iunxiun  3983  iinpw  3992  disjnim  4009  dftr2  4118  dftr5  4119  dftr3  4120  dftr4  4121  vnex  4149  inuni  4173  snelpw  4231  sspwb  4234  opelopabsb  4278  eusv2  4475  orddif  4564  onintexmid  4590  zfregfr  4591  tfi  4599  opthprc  4695  elxp3  4698  xpiundir  4703  elvv  4706  brinxp2  4711  relsn  4749  reliun  4765  inxp  4779  raliunxp  4786  rexiunxp  4787  cnvuni  4831  dm0rn0  4862  elrn  4888  ssdmres  4947  dfres2  4977  dfima2  4990  args  5015  cotr  5028  intasym  5031  asymref  5032  intirr  5033  cnv0  5050  xp11m  5085  cnvresima  5136  resco  5151  rnco  5153  coiun  5156  coass  5165  dfiota2  5197  dffun2  5245  dffun6f  5248  dffun4f  5251  dffun7  5262  dffun9  5264  funfn  5265  svrelfun  5300  imadiflem  5314  dffn2  5386  dffn3  5395  fintm  5420  dffn4  5463  dff1o4  5488  brprcneu  5527  eqfnfv3  5636  fnreseql  5647  fsn  5709  abrexco  5781  imaiun  5782  mpo2eqb  6007  elovmpo  6096  abexex  6152  releldm2  6211  fnmpo  6228  dftpos4  6289  tfrlem7  6343  0er  6594  eroveu  6653  erovlem  6654  map0e  6713  elixpconst  6733  domen  6778  reuen1  6828  xpf1o  6873  ssfilem  6904  finexdc  6931  pw1dc0el  6940  ssfirab  6963  sbthlemi10  6996  djuexb  7074  dmaddpq  7409  dmmulpq  7410  distrnqg  7417  enq0enq  7461  enq0tr  7464  nqnq0pi  7468  distrnq0  7489  prltlu  7517  prarloc  7533  genpdflem  7537  ltexprlemm  7630  ltexprlemlol  7632  ltexprlemupu  7634  ltexprlemdisj  7636  recexprlemdisj  7660  ltresr  7869  elnnz  9294  dfz2  9356  2rexuz  9614  eluz2b1  9633  elxr  9808  elixx1  9929  elioo2  9953  elioopnf  9999  elicopnf  10001  elfz1  10045  fzdifsuc  10113  fznn  10121  fzp1nel  10136  fznn0  10145  dfrp2  10296  redivap  10918  imdivap  10925  rexanre  11264  climreu  11340  prodmodc  11621  3dvdsdec  11905  3dvds2dec  11906  bezoutlembi  12041  nnwosdc  12075  isprm2  12152  isprm3  12153  isprm4  12154  pythagtriplem2  12301  elgz  12406  inffinp1  12483  isnsg4  13168  isrng  13305  isring  13371  dfrhm2  13521  lss1d  13716  isbasis3g  14023  restsn  14157  lmbr  14190  txbas  14235  tx2cn  14247  elcncf1di  14543  dedekindicclemicc  14587  limcrcl  14604  bj-nnor  14964  bj-vprc  15126  ss1oel2o  15222  subctctexmid  15229  trirec0xor  15272