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  616  mpbiran  949  mpbiran2  950  3anrev  1015  an6  1358  nfand  1617  19.33b2  1678  nf3  1717  nf4dc  1718  nf4r  1719  equsalh  1774  sb6x  1828  sb5f  1853  sbidm  1900  equsv  1934  sb5  1938  sbanv  1940  sborv  1941  sbhb  1996  sb3an  2014  sbel2x  2054  sbal1yz  2057  sbexyz  2059  eu2  2127  2eu4  2176  cleqh  2334  cleqf  2411  dcne  2425  necon3bii  2452  ne3anior  2502  r2alf  2561  r2exf  2562  r19.23t  2652  r19.26-3  2675  r19.26m  2676  r19.43  2703  rabid2  2723  isset  2822  ralv  2833  rexv  2834  reuv  2835  rmov  2836  rexcom4b  2841  ceqsex4v  2860  ceqsex8v  2862  ceqsrexv  2950  ralrab2  2985  rexrab2  2987  reu2  3008  reu3  3010  reueq  3019  2reuswapdc  3024  reuind  3025  sbc3an  3107  rmo2ilem  3136  csbcow  3152  ssalel  3229  dfss3  3230  dfss3f  3234  ssabral  3313  rabss  3319  ssrabeq  3330  uniiunlem  3332  dfdif3  3333  ddifstab  3355  uncom  3367  inass  3435  indi  3472  difindiss  3479  difin2  3487  reupick3  3510  n0rf  3525  eq0  3531  eqv  3532  vss  3560  disj  3561  disj3  3565  undisj1  3570  undisj2  3571  exsnrex  3736  euabsn2  3765  euabsn  3766  snmb  3818  prssg  3856  dfuni2  3921  unissb  3949  elint2  3961  ssint  3970  dfiin2g  4029  iunn0m  4057  iunxun  4076  iunxiun  4078  iinpw  4087  disjnim  4104  dftr2  4215  dftr5  4216  dftr3  4217  dftr4  4218  vnex  4246  inuni  4272  snelpw  4333  sspwb  4337  opelopabsb  4383  eusv2  4583  orddif  4674  onintexmid  4700  zfregfr  4701  tfi  4709  opthprc  4806  elxp3  4809  xpiundir  4814  elvv  4817  brinxp2  4822  relsn  4860  reliun  4878  inxp  4894  raliunxp  4901  rexiunxp  4902  cnvuni  4946  dm0rn0  4978  elrn  5005  ssdmres  5065  dfres2  5095  dfima2  5108  args  5136  cotr  5149  intasym  5152  asymref  5153  intirr  5154  cnv0  5171  xp11m  5206  cnvresima  5257  resco  5272  rnco  5274  coiun  5277  coass  5286  dfiota2  5318  dffun2  5367  dffun6f  5370  dffun4f  5373  dffun7  5384  dffun9  5386  funfn  5387  svrelfun  5426  imadiflem  5440  dffn2  5515  dffn3  5524  fintm  5557  dffn4  5601  dff1o4  5627  brprcneu  5668  eqfnfv3  5782  fnreseql  5793  fsn  5854  abrexco  5938  imaiun  5939  mpo2eqb  6171  elovmpo  6261  abexex  6328  releldm2  6392  fnmpo  6411  cnvimadfsn  6458  dftpos4  6507  tfrlem7  6561  0er  6814  eroveu  6873  erovlem  6874  map0e  6933  elixpconst  6954  domen  7001  reuen1  7054  xpf1o  7110  ssfilem  7143  ssfilemd  7145  finexdc  7173  pw1dc0el  7184  ssfirab  7210  sbthlemi10  7249  djuexb  7348  sspw1or2  7508  iftrueb01  7546  pw1if  7548  dmaddpq  7710  dmmulpq  7711  distrnqg  7718  enq0enq  7762  enq0tr  7765  nqnq0pi  7769  distrnq0  7790  prltlu  7818  prarloc  7834  genpdflem  7838  ltexprlemm  7931  ltexprlemlol  7933  ltexprlemupu  7935  ltexprlemdisj  7937  recexprlemdisj  7961  ltresr  8170  elnnz  9607  dfz2  9670  2rexuz  9935  eluz2b1  9954  elxr  10131  elixx1  10252  elioo2  10276  elioopnf  10322  elicopnf  10324  elfz1  10369  fzdifsuc  10440  fznn  10448  fzp1nel  10463  fznn0  10472  dfrp2  10650  redivap  11587  imdivap  11594  rexanre  11933  climreu  12010  prodmodc  12292  3dvdsdec  12579  3dvds2dec  12580  bitsval  12657  bezoutlembi  12729  nnwosdc  12763  isprm2  12842  isprm3  12843  isprm4  12844  pythagtriplem2  12992  elgz  13097  inffinp1  13267  isnsg4  13968  isrng  14176  isring  14246  dfrhm2  14402  lss1d  14660  isbasis3g  15040  restsn  15174  lmbr  15207  txbas  15252  tx2cn  15264  elcncf1di  15573  dedekindicclemicc  15626  limcrcl  15652  isclwwlk  16518  clwwlkccatlem  16524  eupth2lem1  16582  bj-nnor  16645  bj-vprc  16805  ss1oel2o  16900  subctctexmid  16913  trirec0xor  16968