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  2022  sbco4  2060  elsb1  2209  elsb2  2210  abeq1i  2343  cbvabw  2354  r19.41  2688  rexcom4a  2827  moeq  2981  mosubt  2983  2reuswapdc  3010  nfcdeq  3028  sbcid  3047  sbcco2  3054  sbc7  3058  sbcie2g  3065  eqsbc1  3071  sbcralt  3108  sbcrext  3109  cbvralcsf  3190  cbvrexcsf  3191  cbvrabcsf  3193  abss  3296  ssab  3297  difrab  3481  abn0m  3520  prsspw  3848  disjnim  4078  brab1  4136  unopab  4168  exss  4319  uniuni  4548  elvvv  4789  eliunxp  4869  ralxp  4873  rexxp  4874  opelco  4902  reldm0  4949  resieq  5023  resiexg  5058  iss  5059  imai  5092  cnvsym  5120  intasym  5121  asymref  5122  codir  5125  poirr2  5129  rninxp  5180  cnvsom  5280  funopg  5360  fin  5523  f1cnvcnv  5553  fndmin  5754  resoprab  6117  mpo2eqb  6131  ov6g  6160  offval  6243  dfopab2  6352  dfoprab3s  6353  fmpox  6365  spc2ed  6398  brtpos0  6418  dftpos3  6428  tpostpos  6430  ercnv  6723  xpcomco  7010  xpassen  7014  phpm  7052  ctssdccl  7310  elni2  7534  elfz2nn0  10347  elfzmlbp  10367  clim0  11847  nnwosdc  12612  isstructim  13098  xpscf  13432  srgrmhm  14010  ntreq0  14859  cnmptcom  15025  dedekindicclemicc  15359