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  687  orordi  781  orordir  782  sbco3v  2023  sbco4  2061  elsb1  2210  elsb2  2211  abeq1i  2344  cbvabw  2357  r19.41  2698  rexcom4a  2837  moeq  2991  mosubt  2993  2reuswapdc  3020  nfcdeq  3038  sbcid  3057  sbcco2  3064  sbc7  3068  sbcie2g  3075  eqsbc1  3081  sbcralt  3118  sbcrext  3119  cbvralcsf  3200  cbvrexcsf  3201  cbvrabcsf  3203  abss  3306  ssab  3307  difrab  3494  abn0m  3533  prsspw  3868  disjnim  4098  brab1  4156  unopab  4188  exss  4342  uniuni  4571  elvvv  4812  eliunxp  4893  ralxp  4897  rexxp  4898  opelco  4926  reldm0  4973  resieq  5047  resiexg  5082  iss  5083  imai  5117  cnvsym  5145  intasym  5146  asymref  5147  codir  5150  poirr2  5154  rninxp  5205  cnvsom  5305  funopg  5385  fin  5552  f1cnvcnv  5583  fndmin  5784  resoprab  6148  mpo2eqb  6162  ov6g  6191  offval  6273  dfopab2  6382  dfoprab3s  6383  fmpox  6395  spc2ed  6428  brtpos0  6482  dftpos3  6492  tpostpos  6494  ercnv  6787  xpcomco  7076  xpassen  7080  phpm  7119  ctssdccl  7401  elni2  7625  elfz2nn0  10442  elfzmlbp  10462  clim0  11963  nnwosdc  12728  isstructim  13215  xpscf  13549  srgrmhm  14127  ntreq0  14984  cnmptcom  15150  dedekindicclemicc  15484