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  2807  ralv  2818  rexv  2819  reuv  2820  rmov  2821  rexcom4b  2826  ceqsex4v  2845  ceqsex8v  2847  ceqsrexv  2934  ralrab2  2969  rexrab2  2971  reu2  2992  reu3  2994  reueq  3003  2reuswapdc  3008  reuind  3009  sbc3an  3091  rmo2ilem  3120  csbcow  3136  ssalel  3213  dfss3  3214  dfss3f  3217  ssabral  3296  rabss  3302  ssrabeq  3312  uniiunlem  3314  dfdif3  3315  ddifstab  3337  uncom  3349  inass  3415  indi  3452  difindiss  3459  difin2  3467  reupick3  3490  n0rf  3505  eq0  3511  eqv  3512  vss  3540  disj  3541  disj3  3545  undisj1  3550  undisj2  3551  exsnrex  3709  euabsn2  3738  euabsn  3739  snmb  3791  prssg  3828  dfuni2  3893  unissb  3921  elint2  3933  ssint  3942  dfiin2g  4001  iunn0m  4029  iunxun  4048  iunxiun  4050  iinpw  4059  disjnim  4076  dftr2  4187  dftr5  4188  dftr3  4189  dftr4  4190  vnex  4218  inuni  4243  snelpw  4302  sspwb  4306  opelopabsb  4352  eusv2  4552  orddif  4643  onintexmid  4669  zfregfr  4670  tfi  4678  opthprc  4775  elxp3  4778  xpiundir  4783  elvv  4786  brinxp2  4791  relsn  4829  reliun  4846  inxp  4862  raliunxp  4869  rexiunxp  4870  cnvuni  4914  dm0rn0  4946  elrn  4973  ssdmres  5033  dfres2  5063  dfima2  5076  args  5103  cotr  5116  intasym  5119  asymref  5120  intirr  5121  cnv0  5138  xp11m  5173  cnvresima  5224  resco  5239  rnco  5241  coiun  5244  coass  5253  dfiota2  5285  dffun2  5334  dffun6f  5337  dffun4f  5340  dffun7  5351  dffun9  5353  funfn  5354  svrelfun  5392  imadiflem  5406  dffn2  5481  dffn3  5490  fintm  5519  dffn4  5562  dff1o4  5588  brprcneu  5628  eqfnfv3  5742  fnreseql  5753  fsn  5815  abrexco  5895  imaiun  5896  mpo2eqb  6126  elovmpo  6216  abexex  6283  releldm2  6343  fnmpo  6362  dftpos4  6424  tfrlem7  6478  0er  6731  eroveu  6790  erovlem  6791  map0e  6850  elixpconst  6870  domen  6917  reuen1  6970  xpf1o  7025  ssfilem  7057  ssfilemd  7059  finexdc  7087  pw1dc0el  7098  ssfirab  7123  sbthlemi10  7159  djuexb  7237  iftrueb01  7434  pw1if  7436  dmaddpq  7592  dmmulpq  7593  distrnqg  7600  enq0enq  7644  enq0tr  7647  nqnq0pi  7651  distrnq0  7672  prltlu  7700  prarloc  7716  genpdflem  7720  ltexprlemm  7813  ltexprlemlol  7815  ltexprlemupu  7817  ltexprlemdisj  7819  recexprlemdisj  7843  ltresr  8052  elnnz  9482  dfz2  9545  2rexuz  9809  eluz2b1  9828  elxr  10004  elixx1  10125  elioo2  10149  elioopnf  10195  elicopnf  10197  elfz1  10241  fzdifsuc  10309  fznn  10317  fzp1nel  10332  fznn0  10341  dfrp2  10516  redivap  11428  imdivap  11435  rexanre  11774  climreu  11851  prodmodc  12132  3dvdsdec  12419  3dvds2dec  12420  bitsval  12497  bezoutlembi  12569  nnwosdc  12603  isprm2  12682  isprm3  12683  isprm4  12684  pythagtriplem2  12832  elgz  12937  inffinp1  13043  isnsg4  13792  isrng  13940  isring  14006  dfrhm2  14161  lss1d  14390  isbasis3g  14763  restsn  14897  lmbr  14930  txbas  14975  tx2cn  14987  elcncf1di  15296  dedekindicclemicc  15349  limcrcl  15375  isclwwlk  16203  clwwlkccatlem  16209  bj-nnor  16280  bj-vprc  16441  ss1oel2o  16536  subctctexmid  16551  trirec0xor  16599