Theorem bitr3i 186

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

Syntax hints:   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitrri  207  3bitr3i  210  3bitr3ri  211  anandi  590  anandir  591  xchnxbi  681  orordi  774  orordir  775  sbco3v  1988  sbco4  2026  elsb1  2174  elsb2  2175  abeq1i  2308  cbvabw  2319  r19.41  2652  rexcom4a  2787  moeq  2939  mosubt  2941  2reuswapdc  2968  nfcdeq  2986  sbcid  3005  sbcco2  3012  sbc7  3016  sbcie2g  3023  eqsbc1  3029  sbcralt  3066  sbcrext  3067  cbvralcsf  3147  cbvrexcsf  3148  cbvrabcsf  3150  abss  3252  ssab  3253  difrab  3437  abn0m  3476  prsspw  3795  disjnim  4024  brab1  4080  unopab  4112  exss  4260  uniuni  4486  elvvv  4726  eliunxp  4805  ralxp  4809  rexxp  4810  opelco  4838  reldm0  4884  resieq  4956  resiexg  4991  iss  4992  imai  5025  cnvsym  5053  intasym  5054  asymref  5055  codir  5058  poirr2  5062  rninxp  5113  cnvsom  5213  funopg  5292  fin  5444  f1cnvcnv  5474  fndmin  5669  resoprab  6018  mpo2eqb  6032  ov6g  6061  offval  6143  dfopab2  6247  dfoprab3s  6248  fmpox  6258  spc2ed  6291  brtpos0  6310  dftpos3  6320  tpostpos  6322  ercnv  6613  xpcomco  6885  xpassen  6889  phpm  6926  ctssdccl  7177  elni2  7381  elfz2nn0  10187  elfzmlbp  10207  clim0  11450  nnwosdc  12206  isstructim  12692  xpscf  12990  srgrmhm  13550  ntreq0  14368  cnmptcom  14534  dedekindicclemicc  14868