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  592  anandir  593  xchnxbi  684  orordi  777  orordir  778  sbco3v  2000  sbco4  2038  elsb1  2187  elsb2  2188  abeq1i  2321  cbvabw  2332  r19.41  2666  rexcom4a  2804  moeq  2958  mosubt  2960  2reuswapdc  2987  nfcdeq  3005  sbcid  3024  sbcco2  3031  sbc7  3035  sbcie2g  3042  eqsbc1  3048  sbcralt  3085  sbcrext  3086  cbvralcsf  3167  cbvrexcsf  3168  cbvrabcsf  3170  abss  3273  ssab  3274  difrab  3458  abn0m  3497  prsspw  3822  disjnim  4052  brab1  4110  unopab  4142  exss  4292  uniuni  4519  elvvv  4759  eliunxp  4838  ralxp  4842  rexxp  4843  opelco  4871  reldm0  4918  resieq  4991  resiexg  5026  iss  5027  imai  5060  cnvsym  5088  intasym  5089  asymref  5090  codir  5093  poirr2  5097  rninxp  5148  cnvsom  5248  funopg  5328  fin  5488  f1cnvcnv  5518  fndmin  5715  resoprab  6071  mpo2eqb  6085  ov6g  6114  offval  6196  dfopab2  6305  dfoprab3s  6306  fmpox  6316  spc2ed  6349  brtpos0  6368  dftpos3  6378  tpostpos  6380  ercnv  6671  xpcomco  6953  xpassen  6957  phpm  6995  ctssdccl  7246  elni2  7469  elfz2nn0  10276  elfzmlbp  10296  clim0  11762  nnwosdc  12526  isstructim  13012  xpscf  13346  srgrmhm  13923  ntreq0  14771  cnmptcom  14937  dedekindicclemicc  15271