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  694  pm4.15  696  3or6  1336  sbal1yz  2030  2exsb  2038  moanim  2129  2eu4  2148  cvjust  2201  abbi  2320  sbc8g  3007  ss2rab  3270  unass  3331  unss  3348  undi  3422  difindiss  3428  notm0  3482  disj  3510  unopab  4127  eqvinop  4291  pwexb  4525  dmun  4890  reldm0  4901  dmres  4985  imadmrn  5037  ssrnres  5130  dmsnm  5153  coundi  5189  coundir  5190  cnvpom  5230  xpcom  5234  fun11  5346  fununi  5347  funcnvuni  5348  isarep1  5365  fsn  5759  fconstfvm  5809  eufnfv  5822  acexmidlem2  5948  eloprabga  6039  funoprabg  6051  ralrnmpo  6067  rexrnmpo  6068  oprabrexex2  6222  dfer2  6628  euen1b  6902  xpsnen  6923  rexuz3  11345  imasaddfnlemg  13190  subsubrng2  14021  subsubrg2  14052  tgval2  14567  ssntr  14638  metrest  15022  plyun0  15252  sinhalfpilem  15307  2lgslem4  15624