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  692  pm4.15  694  3or6  1323  sbal1yz  2001  2exsb  2009  moanim  2100  2eu4  2119  cvjust  2172  abbi  2291  sbc8g  2972  ss2rab  3233  unass  3294  unss  3311  undi  3385  difindiss  3391  notm0  3445  disj  3473  unopab  4084  eqvinop  4245  pwexb  4476  dmun  4836  reldm0  4847  dmres  4930  imadmrn  4982  ssrnres  5073  dmsnm  5096  coundi  5132  coundir  5133  cnvpom  5173  xpcom  5177  fun11  5285  fununi  5286  funcnvuni  5287  isarep1  5304  fsn  5690  fconstfvm  5736  eufnfv  5749  acexmidlem2  5874  eloprabga  5964  funoprabg  5976  ralrnmpo  5991  rexrnmpo  5992  oprabrexex2  6133  dfer2  6538  euen1b  6805  xpsnen  6823  rexuz3  11001  imasaddfnlemg  12740  subsubrg2  13372  tgval2  13590  ssntr  13661  metrest  14045  sinhalfpilem  14251