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  614  mpbiran  945  mpbiran2  946  3anrev  993  an6  1336  nfand  1594  19.33b2  1655  nf3  1695  nf4dc  1696  nf4r  1697  equsalh  1752  sb6x  1805  sb5f  1830  sbidm  1877  sb5  1914  sbanv  1916  sborv  1917  sbhb  1971  sb3an  1989  sbel2x  2029  sbal1yz  2032  sbexyz  2034  eu2  2102  2eu4  2151  cleqh  2309  cleqf  2377  dcne  2391  necon3bii  2418  ne3anior  2468  r2alf  2527  r2exf  2528  r19.23t  2618  r19.26-3  2641  r19.26m  2642  r19.43  2669  rabid2  2688  isset  2786  ralv  2797  rexv  2798  reuv  2799  rmov  2800  rexcom4b  2805  ceqsex4v  2824  ceqsex8v  2826  ceqsrexv  2913  ralrab2  2948  rexrab2  2950  reu2  2971  reu3  2973  reueq  2982  2reuswapdc  2987  reuind  2988  sbc3an  3070  rmo2ilem  3099  csbcow  3115  ssalel  3192  dfss3  3193  dfss3f  3196  ssabral  3275  rabss  3281  ssrabeq  3291  uniiunlem  3293  dfdif3  3294  ddifstab  3316  uncom  3328  inass  3394  indi  3431  difindiss  3438  difin2  3446  reupick3  3469  n0rf  3484  eq0  3490  eqv  3491  vss  3519  disj  3520  disj3  3524  undisj1  3529  undisj2  3530  exsnrex  3688  euabsn2  3715  euabsn  3716  snmb  3767  prssg  3804  dfuni2  3869  unissb  3897  elint2  3909  ssint  3918  dfiin2g  3977  iunn0m  4005  iunxun  4024  iunxiun  4026  iinpw  4035  disjnim  4052  dftr2  4163  dftr5  4164  dftr3  4165  dftr4  4166  vnex  4194  inuni  4218  snelpw  4277  sspwb  4281  opelopabsb  4327  eusv2  4525  orddif  4616  onintexmid  4642  zfregfr  4643  tfi  4651  opthprc  4747  elxp3  4750  xpiundir  4755  elvv  4758  brinxp2  4763  relsn  4801  reliun  4817  inxp  4833  raliunxp  4840  rexiunxp  4841  cnvuni  4885  dm0rn0  4917  elrn  4943  ssdmres  5003  dfres2  5033  dfima2  5046  args  5073  cotr  5086  intasym  5089  asymref  5090  intirr  5091  cnv0  5108  xp11m  5143  cnvresima  5194  resco  5209  rnco  5211  coiun  5214  coass  5223  dfiota2  5255  dffun2  5304  dffun6f  5307  dffun4f  5310  dffun7  5321  dffun9  5323  funfn  5324  svrelfun  5362  imadiflem  5376  dffn2  5451  dffn3  5460  fintm  5487  dffn4  5530  dff1o4  5556  brprcneu  5596  eqfnfv3  5707  fnreseql  5718  fsn  5780  abrexco  5856  imaiun  5857  mpo2eqb  6085  elovmpo  6175  abexex  6241  releldm2  6301  fnmpo  6318  dftpos4  6379  tfrlem7  6433  0er  6684  eroveu  6743  erovlem  6744  map0e  6803  elixpconst  6823  domen  6870  reuen1  6923  xpf1o  6973  ssfilem  7005  finexdc  7032  pw1dc0el  7041  ssfirab  7066  sbthlemi10  7101  djuexb  7179  iftrueb01  7376  pw1if  7378  dmaddpq  7534  dmmulpq  7535  distrnqg  7542  enq0enq  7586  enq0tr  7589  nqnq0pi  7593  distrnq0  7614  prltlu  7642  prarloc  7658  genpdflem  7662  ltexprlemm  7755  ltexprlemlol  7757  ltexprlemupu  7759  ltexprlemdisj  7761  recexprlemdisj  7785  ltresr  7994  elnnz  9424  dfz2  9487  2rexuz  9745  eluz2b1  9764  elxr  9940  elixx1  10061  elioo2  10085  elioopnf  10131  elicopnf  10133  elfz1  10177  fzdifsuc  10245  fznn  10253  fzp1nel  10268  fznn0  10277  dfrp2  10450  redivap  11351  imdivap  11358  rexanre  11697  climreu  11774  prodmodc  12055  3dvdsdec  12342  3dvds2dec  12343  bitsval  12420  bezoutlembi  12492  nnwosdc  12526  isprm2  12605  isprm3  12606  isprm4  12607  pythagtriplem2  12755  elgz  12860  inffinp1  12966  isnsg4  13715  isrng  13863  isring  13929  dfrhm2  14083  lss1d  14312  isbasis3g  14685  restsn  14819  lmbr  14852  txbas  14897  tx2cn  14909  elcncf1di  15218  dedekindicclemicc  15271  limcrcl  15297  bj-nnor  16008  bj-vprc  16169  ss1oel2o  16265  subctctexmid  16277  trirec0xor  16324