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  555  anandir  556  xchnxbi  638  orordi  723  orordir  724  sbco3v  1885  elsb3  1894  elsb4  1895  sbco4  1925  abeq1i  2191  r19.41  2510  rexcom4a  2624  moeq  2768  mosubt  2770  2reuswapdc  2795  nfcdeq  2813  sbcid  2831  sbcco2  2838  sbc7  2842  sbcie2g  2848  eqsbc3  2854  sbcralt  2891  sbcrext  2892  cbvralcsf  2965  cbvrexcsf  2966  cbvrabcsf  2968  abss  3064  ssab  3065  difrab  3245  prsspw  3565  brab1  3838  unopab  3865  exss  3990  uniuni  4209  elvvv  4429  eliunxp  4503  ralxp  4507  rexxp  4508  opelco  4535  reldm0  4581  resieq  4650  resiexg  4683  iss  4684  imai  4711  cnvsym  4738  intasym  4739  asymref  4740  codir  4743  poirr2  4747  rninxp  4794  cnvsom  4891  funopg  4964  fin  5107  f1cnvcnv  5131  fndmin  5306  resoprab  5628  mpt22eqb  5641  ov6g  5669  offval  5750  dfopab2  5846  dfoprab3s  5847  fmpt2x  5857  spc2ed  5885  brtpos0  5901  dftpos3  5911  tpostpos  5913  ercnv  6193  xpcomco  6370  xpassen  6374  phpm  6400  elni2  6566  elfz2nn0  9205  elfzmlbp  9220  clim0  10262