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  946  mpbiran2  947  3anrev  1012  an6  1355  nfand  1614  19.33b2  1675  nf3  1715  nf4dc  1716  nf4r  1717  equsalh  1772  sb6x  1825  sb5f  1850  sbidm  1897  sb5  1934  sbanv  1936  sborv  1937  sbhb  1991  sb3an  2009  sbel2x  2049  sbal1yz  2052  sbexyz  2054  eu2  2122  2eu4  2171  cleqh  2329  cleqf  2397  dcne  2411  necon3bii  2438  ne3anior  2488  r2alf  2547  r2exf  2548  r19.23t  2638  r19.26-3  2661  r19.26m  2662  r19.43  2689  rabid2  2708  isset  2806  ralv  2817  rexv  2818  reuv  2819  rmov  2820  rexcom4b  2825  ceqsex4v  2844  ceqsex8v  2846  ceqsrexv  2933  ralrab2  2968  rexrab2  2970  reu2  2991  reu3  2993  reueq  3002  2reuswapdc  3007  reuind  3008  sbc3an  3090  rmo2ilem  3119  csbcow  3135  ssalel  3212  dfss3  3213  dfss3f  3216  ssabral  3295  rabss  3301  ssrabeq  3311  uniiunlem  3313  dfdif3  3314  ddifstab  3336  uncom  3348  inass  3414  indi  3451  difindiss  3458  difin2  3466  reupick3  3489  n0rf  3504  eq0  3510  eqv  3511  vss  3539  disj  3540  disj3  3544  undisj1  3549  undisj2  3550  exsnrex  3708  euabsn2  3735  euabsn  3736  snmb  3788  prssg  3825  dfuni2  3890  unissb  3918  elint2  3930  ssint  3939  dfiin2g  3998  iunn0m  4026  iunxun  4045  iunxiun  4047  iinpw  4056  disjnim  4073  dftr2  4184  dftr5  4185  dftr3  4186  dftr4  4187  vnex  4215  inuni  4239  snelpw  4298  sspwb  4302  opelopabsb  4348  eusv2  4548  orddif  4639  onintexmid  4665  zfregfr  4666  tfi  4674  opthprc  4770  elxp3  4773  xpiundir  4778  elvv  4781  brinxp2  4786  relsn  4824  reliun  4840  inxp  4856  raliunxp  4863  rexiunxp  4864  cnvuni  4908  dm0rn0  4940  elrn  4967  ssdmres  5027  dfres2  5057  dfima2  5070  args  5097  cotr  5110  intasym  5113  asymref  5114  intirr  5115  cnv0  5132  xp11m  5167  cnvresima  5218  resco  5233  rnco  5235  coiun  5238  coass  5247  dfiota2  5279  dffun2  5328  dffun6f  5331  dffun4f  5334  dffun7  5345  dffun9  5347  funfn  5348  svrelfun  5386  imadiflem  5400  dffn2  5475  dffn3  5484  fintm  5513  dffn4  5556  dff1o4  5582  brprcneu  5622  eqfnfv3  5736  fnreseql  5747  fsn  5809  abrexco  5889  imaiun  5890  mpo2eqb  6120  elovmpo  6210  abexex  6277  releldm2  6337  fnmpo  6354  dftpos4  6415  tfrlem7  6469  0er  6722  eroveu  6781  erovlem  6782  map0e  6841  elixpconst  6861  domen  6908  reuen1  6961  xpf1o  7013  ssfilem  7045  finexdc  7072  pw1dc0el  7081  ssfirab  7106  sbthlemi10  7141  djuexb  7219  iftrueb01  7416  pw1if  7418  dmaddpq  7574  dmmulpq  7575  distrnqg  7582  enq0enq  7626  enq0tr  7629  nqnq0pi  7633  distrnq0  7654  prltlu  7682  prarloc  7698  genpdflem  7702  ltexprlemm  7795  ltexprlemlol  7797  ltexprlemupu  7799  ltexprlemdisj  7801  recexprlemdisj  7825  ltresr  8034  elnnz  9464  dfz2  9527  2rexuz  9785  eluz2b1  9804  elxr  9980  elixx1  10101  elioo2  10125  elioopnf  10171  elicopnf  10173  elfz1  10217  fzdifsuc  10285  fznn  10293  fzp1nel  10308  fznn0  10317  dfrp2  10491  redivap  11393  imdivap  11400  rexanre  11739  climreu  11816  prodmodc  12097  3dvdsdec  12384  3dvds2dec  12385  bitsval  12462  bezoutlembi  12534  nnwosdc  12568  isprm2  12647  isprm3  12648  isprm4  12649  pythagtriplem2  12797  elgz  12902  inffinp1  13008  isnsg4  13757  isrng  13905  isring  13971  dfrhm2  14126  lss1d  14355  isbasis3g  14728  restsn  14862  lmbr  14895  txbas  14940  tx2cn  14952  elcncf1di  15261  dedekindicclemicc  15314  limcrcl  15340  bj-nnor  16122  bj-vprc  16283  ss1oel2o  16380  subctctexmid  16395  trirec0xor  16443