Theorem bitr2i 185

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr2i.1	⊢ (𝜑 ↔ 𝜓)
bitr2i.2	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
bitr2i	⊢ (𝜒 ↔ 𝜑)

Proof of Theorem bitr2i

Step	Hyp	Ref	Expression
1		bitr2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		bitr2i.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3	1, 2	bitri 184	. 2 ⊢ (𝜑 ↔ 𝜒)
4	3	bicomi 132	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  3bitr2ri  209  3bitr4ri  213  nan  699  pm4.15  702  3or6  1360  sbal1yz  2055  2exsb  2063  moanim  2155  2eu4  2174  cvjust  2227  abbibcom  2346  sbc8g  3049  ss2rab  3313  unass  3375  unss  3392  undi  3468  difindiss  3474  notm0  3528  disj  3556  unopab  4188  eqvinop  4358  pwexb  4594  dmun  4962  reldm0  4973  dmres  5058  imadmrn  5110  ssrnres  5204  dmsnm  5227  coundi  5263  coundir  5264  cnvpom  5304  xpcom  5308  fun11  5422  fununi  5423  funcnvuni  5424  isarep1  5441  fsn  5848  fconstfvm  5901  eufnfv  5916  acexmidlem2  6046  eloprabga  6139  funoprabg  6151  ralrnmpo  6167  rexrnmpo  6168  oprabrexex2  6322  dfer2  6767  euen1b  7042  xpsnen  7071  rexuz3  11668  imasaddfnlemg  13516  subsubrng2  14349  subsubrg2  14380  tgval2  14903  ssntr  14974  metrest  15358  plyun0  15588  sinhalfpilem  15643  2lgslem4  15963  wlkeq  16336  clwwlkn1  16400  clwwlkn2  16403  clwwlknon2x  16417