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  594  anandir  595  xchnxbi  686  orordi  780  orordir  781  sbco3v  2021  sbco4  2059  elsb1  2208  elsb2  2209  abeq1i  2342  cbvabw  2353  r19.41  2687  rexcom4a  2826  moeq  2980  mosubt  2982  2reuswapdc  3009  nfcdeq  3027  sbcid  3046  sbcco2  3053  sbc7  3057  sbcie2g  3064  eqsbc1  3070  sbcralt  3107  sbcrext  3108  cbvralcsf  3189  cbvrexcsf  3190  cbvrabcsf  3192  abss  3295  ssab  3296  difrab  3480  abn0m  3519  prsspw  3849  disjnim  4079  brab1  4137  unopab  4169  exss  4321  uniuni  4550  elvvv  4791  eliunxp  4871  ralxp  4875  rexxp  4876  opelco  4904  reldm0  4951  resieq  5025  resiexg  5060  iss  5061  imai  5094  cnvsym  5122  intasym  5123  asymref  5124  codir  5127  poirr2  5131  rninxp  5182  cnvsom  5282  funopg  5362  fin  5525  f1cnvcnv  5556  fndmin  5757  resoprab  6122  mpo2eqb  6136  ov6g  6165  offval  6248  dfopab2  6357  dfoprab3s  6358  fmpox  6370  spc2ed  6403  brtpos0  6423  dftpos3  6433  tpostpos  6435  ercnv  6728  xpcomco  7015  xpassen  7019  phpm  7057  ctssdccl  7315  elni2  7539  elfz2nn0  10352  elfzmlbp  10372  clim0  11868  nnwosdc  12633  isstructim  13119  xpscf  13453  srgrmhm  14031  ntreq0  14885  cnmptcom  15051  dedekindicclemicc  15385