Theorem bitr4i 185

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 130	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	bitri 182	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3bitr2i  206  3bitr2ri  207  3bitr4i  210  3bitr4ri  211  imdistan  432  mpbiran  881  mpbiran2  882  3anrev  929  an6  1252  nfand  1500  19.33b2  1560  nf3  1599  nf4dc  1600  nf4r  1601  equsalh  1654  sb6x  1702  sb5f  1725  sbidm  1772  sb5  1808  sbanv  1810  sborv  1811  sbhb  1857  sb3an  1873  sbel2x  1915  sbal1yz  1918  sbexyz  1920  eu2  1985  2eu4  2034  cleqh  2178  cleqf  2242  dcne  2256  necon3bii  2283  ne3anior  2333  r2alf  2383  r2exf  2384  r19.23t  2467  r19.26-3  2487  r19.26m  2488  r19.43  2512  rabid2  2530  isset  2605  ralv  2616  rexv  2617  reuv  2618  rmov  2619  rexcom4b  2624  ceqsex4v  2642  ceqsex8v  2644  ceqsrexv  2725  ralrab2  2757  rexrab2  2759  reu2  2780  reu3  2782  reueq  2789  2reuswapdc  2794  reuind  2795  sbc3an  2875  rmo2ilem  2903  dfss2  2988  dfss3  2989  dfss3f  2991  ssabral  3065  rabss  3071  ssrabeq  3080  uniiunlem  3082  ddifstab  3104  uncom  3116  inass  3176  indi  3211  difindiss  3218  difin2  3226  reupick3  3249  n0rf  3260  eq0  3266  eqv  3267  vss  3291  disj  3292  disj3  3296  undisj1  3301  undisj2  3302  exsnrex  3435  euabsn2  3461  euabsn  3462  prssg  3542  dfuni2  3603  unissb  3631  elint2  3643  ssint  3652  dfiin2g  3711  iunn0m  3738  iunxun  3756  iunxiun  3757  iinpw  3763  dftr2  3877  dftr5  3878  dftr3  3879  dftr4  3880  vprc  3909  inuni  3930  snelpw  3968  sspwb  3971  opelopabsb  4015  eusv2  4207  orddif  4290  onintexmid  4315  zfregfr  4316  tfi  4323  opthprc  4409  elxp3  4412  xpiundir  4417  elvv  4420  brinxp2  4425  relsn  4461  reliun  4476  inxp  4488  raliunxp  4495  rexiunxp  4496  cnvuni  4539  dm0rn0  4570  elrn  4595  ssdmres  4651  dfres2  4678  dfima2  4690  args  4714  cotr  4726  intasym  4729  asymref  4730  intirr  4731  cnv0  4747  xp11m  4779  cnvresima  4830  resco  4845  rnco  4847  coiun  4850  coass  4859  dfiota2  4888  dffun2  4932  dffun6f  4935  dffun4f  4938  dffun7  4948  dffun9  4950  funfn  4951  svrelfun  4984  imadiflem  4998  dffn2  5067  dffn3  5073  fintm  5095  dffn4  5132  dff1o4  5154  brprcneu  5191  eqfnfv3  5288  fnreseql  5298  fsn  5356  abrexco  5419  imaiun  5420  mpt22eqb  5630  elovmpt2  5721  abexex  5773  releldm2  5831  fnmpt2  5848  dftpos4  5901  tfrlem7  5956  0er  6163  eroveu  6220  erovlem  6221  domen  6255  reuen1  6304  ssfilem  6360  dmaddpq  6569  dmmulpq  6570  distrnqg  6577  enq0enq  6621  enq0tr  6624  nqnq0pi  6628  distrnq0  6649  prltlu  6677  prarloc  6693  genpdflem  6697  ltexprlemm  6790  ltexprlemlol  6792  ltexprlemupu  6794  ltexprlemdisj  6796  recexprlemdisj  6820  ltresr  7007  elnnz  8361  dfz2  8420  2rexuz  8670  eluz2b1  8688  elxr  8850  elixx1  8920  elioo2  8944  elioopnf  8990  elicopnf  8992  elfz1  9034  fzdifsuc  9098  fznn  9106  fzp1nel  9121  fznn0  9129  redivap  9761  imdivap  9768  rexanre  10106  climreu  10136  3dvdsdec  10264  3dvds2dec  10265  bezoutlembi  10394  isprm2  10499  isprm3  10500  isprm4  10501  dcdc  10572  bj-vprc  10687