Theorem bitr3i 184

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr3i.1	⊢ (𝜓 ↔ 𝜑)
bitr3i.2	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
bitr3i	⊢ (𝜑 ↔ 𝜒)

Proof of Theorem bitr3i

Step	Hyp	Ref	Expression
1		bitr3i.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	bicomi 130	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3i.2	. 2 ⊢ (𝜓 ↔ 𝜒)
4	2, 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:  3bitrri  205  3bitr3i  208  3bitr3ri  209  anandi  557  anandir  558  xchnxbi  640  orordi  725  orordir  726  sbco3v  1891  elsb3  1900  elsb4  1901  sbco4  1931  abeq1i  2199  r19.41  2522  rexcom4a  2643  moeq  2790  mosubt  2792  2reuswapdc  2819  nfcdeq  2837  sbcid  2855  sbcco2  2862  sbc7  2866  sbcie2g  2872  eqsbc3  2878  sbcralt  2915  sbcrext  2916  cbvralcsf  2990  cbvrexcsf  2991  cbvrabcsf  2993  abss  3090  ssab  3091  difrab  3273  abn0m  3308  prsspw  3609  disjnim  3836  brab1  3890  unopab  3917  exss  4054  uniuni  4273  elvvv  4501  eliunxp  4575  ralxp  4579  rexxp  4580  opelco  4608  reldm0  4654  resieq  4723  resiexg  4757  iss  4758  imai  4788  cnvsym  4815  intasym  4816  asymref  4817  codir  4820  poirr2  4824  rninxp  4874  cnvsom  4974  funopg  5048  fin  5197  f1cnvcnv  5227  fndmin  5406  resoprab  5741  mpt22eqb  5754  ov6g  5782  offval  5863  dfopab2  5959  dfoprab3s  5960  fmpt2x  5970  spc2ed  5998  brtpos0  6017  dftpos3  6027  tpostpos  6029  ercnv  6311  xpcomco  6540  xpassen  6544  phpm  6579  elni2  6871  elfz2nn0  9522  elfzmlbp  9539  clim0  10669  isstructim  11504