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  778  orordir  779  sbco3v  2020  sbco4  2058  elsb1  2207  elsb2  2208  abeq1i  2341  cbvabw  2352  r19.41  2686  rexcom4a  2824  moeq  2978  mosubt  2980  2reuswapdc  3007  nfcdeq  3025  sbcid  3044  sbcco2  3051  sbc7  3055  sbcie2g  3062  eqsbc1  3068  sbcralt  3105  sbcrext  3106  cbvralcsf  3187  cbvrexcsf  3188  cbvrabcsf  3190  abss  3293  ssab  3294  difrab  3478  abn0m  3517  prsspw  3843  disjnim  4073  brab1  4131  unopab  4163  exss  4313  uniuni  4542  elvvv  4782  eliunxp  4861  ralxp  4865  rexxp  4866  opelco  4894  reldm0  4941  resieq  5015  resiexg  5050  iss  5051  imai  5084  cnvsym  5112  intasym  5113  asymref  5114  codir  5117  poirr2  5121  rninxp  5172  cnvsom  5272  funopg  5352  fin  5514  f1cnvcnv  5544  fndmin  5744  resoprab  6106  mpo2eqb  6120  ov6g  6149  offval  6232  dfopab2  6341  dfoprab3s  6342  fmpox  6352  spc2ed  6385  brtpos0  6404  dftpos3  6414  tpostpos  6416  ercnv  6709  xpcomco  6993  xpassen  6997  phpm  7035  ctssdccl  7286  elni2  7509  elfz2nn0  10316  elfzmlbp  10336  clim0  11804  nnwosdc  12568  isstructim  13054  xpscf  13388  srgrmhm  13965  ntreq0  14814  cnmptcom  14980  dedekindicclemicc  15314