Theorem bitr3i 175

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

Syntax hints:   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3bitrri  196  3bitr3i  199  3bitr3ri  200  anandi  524  anandir  525  xchnxbi  605  orordi  690  orordir  691  sbco3v  1843  elsb3  1852  elsb4  1853  sbco4  1883  abeq1i  2149  r19.41  2465  rexcom4a  2578  moeq  2716  mosubt  2718  2reuswapdc  2743  nfcdeq  2761  sbcid  2779  sbcco2  2786  sbc7  2790  sbcie2g  2796  eqsbc3  2802  sbcralt  2834  sbcrext  2835  cbvralcsf  2908  cbvrexcsf  2909  cbvrabcsf  2911  abss  3009  ssab  3010  difrab  3211  prsspw  3536  brab1  3809  unopab  3836  exss  3963  uniuni  4183  elvvv  4403  eliunxp  4475  ralxp  4479  rexxp  4480  opelco  4507  reldm0  4553  resieq  4622  resiexg  4653  iss  4654  imai  4681  cnvsym  4708  intasym  4709  asymref  4710  codir  4713  poirr2  4717  rninxp  4764  cnvsom  4861  funopg  4934  fin  5076  f1cnvcnv  5100  fndmin  5274  resoprab  5597  mpt22eqb  5610  ov6g  5638  offval  5719  dfopab2  5815  dfoprab3s  5816  fmpt2x  5826  brtpos0  5867  dftpos3  5877  tpostpos  5879  ercnv  6127  xpcomco  6300  xpassen  6304  phpm  6327  elni2  6412  elfz2nn0  8973  elfzmlbp  8990  expival  9257  clim0  9806