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  2025  sbco4  2063  elsb1  2212  elsb2  2213  abeq1i  2346  cbvabw  2359  r19.41  2700  rexcom4a  2840  moeq  2994  mosubt  2996  2reuswapdc  3023  nfcdeq  3041  sbcid  3060  sbcco2  3067  sbc7  3071  sbcie2g  3078  eqsbc1  3084  sbcralt  3121  sbcrext  3122  cbvralcsf  3203  cbvrexcsf  3204  cbvrabcsf  3206  abss  3309  ssab  3310  difrab  3497  abn0m  3536  prsspw  3871  disjnim  4101  brab1  4159  unopab  4191  exss  4345  uniuni  4574  elvvv  4815  eliunxp  4896  ralxp  4900  rexxp  4901  opelco  4929  reldm0  4976  resieq  5050  resiexg  5085  iss  5086  imai  5120  cnvsym  5148  intasym  5149  asymref  5150  codir  5153  poirr2  5157  rninxp  5208  cnvsom  5308  funopg  5388  fin  5555  f1cnvcnv  5586  fndmin  5787  resoprab  6151  mpo2eqb  6165  ov6g  6194  offval  6276  dfopab2  6385  dfoprab3s  6386  fmpox  6398  spc2ed  6431  brtpos0  6485  dftpos3  6495  tpostpos  6497  ercnv  6790  xpcomco  7079  xpassen  7083  phpm  7122  ctssdccl  7404  elni2  7634  elfz2nn0  10453  elfzmlbp  10473  clim0  11978  nnwosdc  12743  isstructim  13247  xpscf  13581  srgrmhm  14159  ntreq0  15046  cnmptcom  15212  dedekindicclemicc  15546