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  940  mpbiran2  941  3anrev  988  an6  1321  nfand  1566  19.33b2  1627  nf3  1667  nf4dc  1668  nf4r  1669  equsalh  1724  sb6x  1777  sb5f  1802  sbidm  1849  sb5  1885  sbanv  1887  sborv  1888  sbhb  1938  sb3an  1956  sbel2x  1996  sbal1yz  1999  sbexyz  2001  eu2  2068  2eu4  2117  cleqh  2275  cleqf  2342  dcne  2356  necon3bii  2383  ne3anior  2433  r2alf  2492  r2exf  2493  r19.23t  2582  r19.26-3  2605  r19.26m  2606  r19.43  2633  rabid2  2651  isset  2741  ralv  2752  rexv  2753  reuv  2754  rmov  2755  rexcom4b  2760  ceqsex4v  2778  ceqsex8v  2780  ceqsrexv  2865  ralrab2  2900  rexrab2  2902  reu2  2923  reu3  2925  reueq  2934  2reuswapdc  2939  reuind  2940  sbc3an  3022  rmo2ilem  3050  csbcow  3066  dfss2  3142  dfss3  3143  dfss3f  3145  ssabral  3224  rabss  3230  ssrabeq  3240  uniiunlem  3242  dfdif3  3243  ddifstab  3265  uncom  3277  inass  3343  indi  3380  difindiss  3387  difin2  3395  reupick3  3418  n0rf  3433  eq0  3439  eqv  3440  vss  3468  disj  3469  disj3  3473  undisj1  3478  undisj2  3479  exsnrex  3631  euabsn2  3658  euabsn  3659  prssg  3746  dfuni2  3807  unissb  3835  elint2  3847  ssint  3856  dfiin2g  3915  iunn0m  3942  iunxun  3961  iunxiun  3963  iinpw  3972  disjnim  3989  dftr2  4098  dftr5  4099  dftr3  4100  dftr4  4101  vnex  4129  inuni  4150  snelpw  4207  sspwb  4210  opelopabsb  4254  eusv2  4451  orddif  4540  onintexmid  4566  zfregfr  4567  tfi  4575  opthprc  4671  elxp3  4674  xpiundir  4679  elvv  4682  brinxp2  4687  relsn  4725  reliun  4741  inxp  4754  raliunxp  4761  rexiunxp  4762  cnvuni  4806  dm0rn0  4837  elrn  4863  ssdmres  4922  dfres2  4952  dfima2  4965  args  4990  cotr  5002  intasym  5005  asymref  5006  intirr  5007  cnv0  5024  xp11m  5059  cnvresima  5110  resco  5125  rnco  5127  coiun  5130  coass  5139  dfiota2  5171  dffun2  5218  dffun6f  5221  dffun4f  5224  dffun7  5235  dffun9  5237  funfn  5238  svrelfun  5273  imadiflem  5287  dffn2  5359  dffn3  5368  fintm  5393  dffn4  5436  dff1o4  5461  brprcneu  5500  eqfnfv3  5607  fnreseql  5618  fsn  5680  abrexco  5750  imaiun  5751  mpo2eqb  5974  elovmpo  6062  abexex  6117  releldm2  6176  fnmpo  6193  dftpos4  6254  tfrlem7  6308  0er  6559  eroveu  6616  erovlem  6617  map0e  6676  elixpconst  6696  domen  6741  reuen1  6791  xpf1o  6834  ssfilem  6865  finexdc  6892  pw1dc0el  6901  ssfirab  6923  sbthlemi10  6955  djuexb  7033  dmaddpq  7353  dmmulpq  7354  distrnqg  7361  enq0enq  7405  enq0tr  7408  nqnq0pi  7412  distrnq0  7433  prltlu  7461  prarloc  7477  genpdflem  7481  ltexprlemm  7574  ltexprlemlol  7576  ltexprlemupu  7578  ltexprlemdisj  7580  recexprlemdisj  7604  ltresr  7813  elnnz  9236  dfz2  9298  2rexuz  9555  eluz2b1  9574  elxr  9747  elixx1  9868  elioo2  9892  elioopnf  9938  elicopnf  9940  elfz1  9984  fzdifsuc  10051  fznn  10059  fzp1nel  10074  fznn0  10083  dfrp2  10234  redivap  10851  imdivap  10858  rexanre  11197  climreu  11273  prodmodc  11554  3dvdsdec  11837  3dvds2dec  11838  bezoutlembi  11973  nnwosdc  12007  isprm2  12084  isprm3  12085  isprm4  12086  pythagtriplem2  12233  elgz  12336  inffinp1  12397  isring  12989  isbasis3g  13124  restsn  13260  lmbr  13293  txbas  13338  tx2cn  13350  elcncf1di  13646  dedekindicclemicc  13690  limcrcl  13707  bj-nnor  14055  bj-vprc  14217  ss1oel2o  14312  subctctexmid  14320  trirec0xor  14363