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  sb5  1937  sbanv  1939  sborv  1940  sbhb  1994  sb3an  2012  sbel2x  2052  sbal1yz  2055  sbexyz  2057  eu2  2125  2eu4  2174  cleqh  2332  cleqf  2409  dcne  2423  necon3bii  2450  ne3anior  2500  r2alf  2559  r2exf  2560  r19.23t  2650  r19.26-3  2673  r19.26m  2674  r19.43  2701  rabid2  2720  isset  2819  ralv  2830  rexv  2831  reuv  2832  rmov  2833  rexcom4b  2838  ceqsex4v  2857  ceqsex8v  2859  ceqsrexv  2946  ralrab2  2981  rexrab2  2983  reu2  3004  reu3  3006  reueq  3015  2reuswapdc  3020  reuind  3021  sbc3an  3103  rmo2ilem  3132  csbcow  3148  ssalel  3225  dfss3  3226  dfss3f  3229  ssabral  3308  rabss  3314  ssrabeq  3325  uniiunlem  3327  dfdif3  3328  ddifstab  3350  uncom  3362  inass  3430  indi  3467  difindiss  3474  difin2  3482  reupick3  3505  n0rf  3520  eq0  3526  eqv  3527  vss  3555  disj  3556  disj3  3560  undisj1  3565  undisj2  3566  exsnrex  3730  euabsn2  3759  euabsn  3760  snmb  3812  prssg  3850  dfuni2  3915  unissb  3943  elint2  3955  ssint  3964  dfiin2g  4023  iunn0m  4051  iunxun  4070  iunxiun  4072  iinpw  4081  disjnim  4098  dftr2  4209  dftr5  4210  dftr3  4211  dftr4  4212  vnex  4240  inuni  4266  snelpw  4327  sspwb  4331  opelopabsb  4377  eusv2  4577  orddif  4668  onintexmid  4694  zfregfr  4695  tfi  4703  opthprc  4800  elxp3  4803  xpiundir  4808  elvv  4811  brinxp2  4816  relsn  4854  reliun  4872  inxp  4888  raliunxp  4895  rexiunxp  4896  cnvuni  4940  dm0rn0  4972  elrn  4999  ssdmres  5059  dfres2  5089  dfima2  5102  args  5130  cotr  5143  intasym  5146  asymref  5147  intirr  5148  cnv0  5165  xp11m  5200  cnvresima  5251  resco  5266  rnco  5268  coiun  5271  coass  5280  dfiota2  5312  dffun2  5361  dffun6f  5364  dffun4f  5367  dffun7  5378  dffun9  5380  funfn  5381  svrelfun  5420  imadiflem  5434  dffn2  5509  dffn3  5518  fintm  5551  dffn4  5595  dff1o4  5621  brprcneu  5662  eqfnfv3  5776  fnreseql  5787  fsn  5848  abrexco  5931  imaiun  5932  mpo2eqb  6162  elovmpo  6252  abexex  6318  releldm2  6378  fnmpo  6397  cnvimadfsn  6444  dftpos4  6493  tfrlem7  6547  0er  6800  eroveu  6859  erovlem  6860  map0e  6919  elixpconst  6940  domen  6987  reuen1  7040  xpf1o  7096  ssfilem  7129  ssfilemd  7131  finexdc  7159  pw1dc0el  7170  ssfirab  7196  sbthlemi10  7235  djuexb  7334  sspw1or2  7494  iftrueb01  7532  pw1if  7534  dmaddpq  7690  dmmulpq  7691  distrnqg  7698  enq0enq  7742  enq0tr  7745  nqnq0pi  7749  distrnq0  7770  prltlu  7798  prarloc  7814  genpdflem  7818  ltexprlemm  7911  ltexprlemlol  7913  ltexprlemupu  7915  ltexprlemdisj  7917  recexprlemdisj  7941  ltresr  8150  elnnz  9583  dfz2  9646  2rexuz  9910  eluz2b1  9929  elxr  10105  elixx1  10226  elioo2  10250  elioopnf  10296  elicopnf  10298  elfz1  10343  fzdifsuc  10411  fznn  10419  fzp1nel  10434  fznn0  10443  dfrp2  10619  redivap  11552  imdivap  11559  rexanre  11898  climreu  11975  prodmodc  12257  3dvdsdec  12544  3dvds2dec  12545  bitsval  12622  bezoutlembi  12694  nnwosdc  12728  isprm2  12807  isprm3  12808  isprm4  12809  pythagtriplem2  12957  elgz  13062  inffinp1  13169  isnsg4  13918  isrng  14067  isring  14133  dfrhm2  14288  lss1d  14518  isbasis3g  14898  restsn  15032  lmbr  15065  txbas  15110  tx2cn  15122  elcncf1di  15431  dedekindicclemicc  15484  limcrcl  15510  isclwwlk  16376  clwwlkccatlem  16382  eupth2lem1  16440  bj-nnor  16493  bj-vprc  16653  ss1oel2o  16748  subctctexmid  16761  trirec0xor  16816