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  703  pm4.15  706  3or6  1364  sbal1yz  2061  2exsb  2069  moanim  2161  2eu4  2180  cvjust  2233  abbibcom  2352  sbc8g  3059  ss2rab  3324  unass  3386  unss  3403  undi  3479  difindiss  3485  notm0  3542  disj  3573  unopab  4208  eqvinop  4381  pwexb  4618  dmun  4986  reldm0  4997  dmres  5082  imadmrn  5134  ssrnres  5228  dmsnm  5251  coundi  5287  coundir  5288  cnvpom  5328  xpcom  5332  fun11  5446  fununi  5447  funcnvuni  5448  isarep1  5465  fsn  5874  fconstfvm  5927  eufnfv  5943  fdmrn  6028  acexmidlem2  6076  eloprabga  6169  funoprabg  6181  ralrnmpo  6197  rexrnmpo  6198  oprabrexex2  6357  dfer2  6802  euen1b  7084  xpsnen  7113  rexuz3  11739  ballotfilem2  13211  ballotfilemi1  13228  imasaddfnlemg  13618  subsubrng2  14506  subsubrg2  14537  tgval2  15135  ssntr  15206  metrest  15590  plyun0  15820  sinhalfpilem  15875  2lgslem4  16205  wlkeq  16578  clwwlkn1  16642  clwwlkn2  16645  clwwlknon2x  16659