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  433  mpbiran  882  mpbiran2  883  3anrev  930  an6  1253  nfand  1501  19.33b2  1561  nf3  1600  nf4dc  1601  nf4r  1602  equsalh  1655  sb6x  1703  sb5f  1726  sbidm  1773  sb5  1809  sbanv  1811  sborv  1812  sbhb  1858  sb3an  1874  sbel2x  1916  sbal1yz  1919  sbexyz  1921  eu2  1986  2eu4  2035  cleqh  2179  cleqf  2243  dcne  2257  necon3bii  2284  ne3anior  2334  r2alf  2384  r2exf  2385  r19.23t  2468  r19.26-3  2488  r19.26m  2489  r19.43  2513  rabid2  2531  isset  2606  ralv  2617  rexv  2618  reuv  2619  rmov  2620  rexcom4b  2625  ceqsex4v  2643  ceqsex8v  2645  ceqsrexv  2726  ralrab2  2758  rexrab2  2760  reu2  2781  reu3  2783  reueq  2790  2reuswapdc  2795  reuind  2796  sbc3an  2876  rmo2ilem  2904  dfss2  2989  dfss3  2990  dfss3f  2992  ssabral  3066  rabss  3072  ssrabeq  3081  uniiunlem  3083  ddifstab  3105  uncom  3117  inass  3183  indi  3218  difindiss  3225  difin2  3233  reupick3  3256  n0rf  3267  eq0  3273  eqv  3274  vss  3298  disj  3299  disj3  3303  undisj1  3308  undisj2  3309  exsnrex  3443  euabsn2  3469  euabsn  3470  prssg  3550  dfuni2  3611  unissb  3639  elint2  3651  ssint  3660  dfiin2g  3719  iunn0m  3746  iunxun  3764  iunxiun  3765  iinpw  3771  dftr2  3885  dftr5  3886  dftr3  3887  dftr4  3888  vprc  3917  inuni  3938  snelpw  3976  sspwb  3979  opelopabsb  4023  eusv2  4215  orddif  4298  onintexmid  4323  zfregfr  4324  tfi  4331  opthprc  4417  elxp3  4420  xpiundir  4425  elvv  4428  brinxp2  4433  relsn  4471  reliun  4486  inxp  4498  raliunxp  4505  rexiunxp  4506  cnvuni  4549  dm0rn0  4580  elrn  4605  ssdmres  4661  dfres2  4688  dfima2  4700  args  4724  cotr  4736  intasym  4739  asymref  4740  intirr  4741  cnv0  4757  xp11m  4789  cnvresima  4840  resco  4855  rnco  4857  coiun  4860  coass  4869  dfiota2  4898  dffun2  4942  dffun6f  4945  dffun4f  4948  dffun7  4958  dffun9  4960  funfn  4961  svrelfun  4995  imadiflem  5009  dffn2  5078  dffn3  5084  fintm  5106  dffn4  5143  dff1o4  5165  brprcneu  5202  eqfnfv3  5299  fnreseql  5309  fsn  5367  abrexco  5430  imaiun  5431  mpt22eqb  5641  elovmpt2  5732  abexex  5784  releldm2  5842  fnmpt2  5859  dftpos4  5912  tfrlem7  5966  0er  6206  eroveu  6263  erovlem  6264  domen  6298  reuen1  6348  xpf1o  6385  ssfilem  6410  dmaddpq  6631  dmmulpq  6632  distrnqg  6639  enq0enq  6683  enq0tr  6686  nqnq0pi  6690  distrnq0  6711  prltlu  6739  prarloc  6755  genpdflem  6759  ltexprlemm  6852  ltexprlemlol  6854  ltexprlemupu  6856  ltexprlemdisj  6858  recexprlemdisj  6882  ltresr  7069  elnnz  8442  dfz2  8501  2rexuz  8751  eluz2b1  8769  elxr  8928  elixx1  8996  elioo2  9020  elioopnf  9066  elicopnf  9068  elfz1  9110  fzdifsuc  9174  fznn  9182  fzp1nel  9197  fznn0  9206  redivap  9899  imdivap  9906  rexanre  10244  climreu  10274  3dvdsdec  10409  3dvds2dec  10410  bezoutlembi  10538  isprm2  10643  isprm3  10644  isprm4  10645  dcdc  10723  bj-vprc  10845