Theorem bitr2i 184

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 183	. 2 ⊢ (𝜑 ↔ 𝜒)
4	3	bicomi 131	1 ⊢ (𝜒 ↔ 𝜑)

Syntax hints:   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitrri  206  3bitr2ri  208  3bitr4ri  212  nan  682  pm4.15  684  3or6  1312  sbal1yz  1988  2exsb  1996  moanim  2087  2eu4  2106  cvjust  2159  abbi  2278  sbc8g  2953  ss2rab  3213  unass  3274  unss  3291  undi  3365  difindiss  3371  notm0  3424  disj  3452  unopab  4055  eqvinop  4215  pwexb  4446  dmun  4805  reldm0  4816  dmres  4899  imadmrn  4950  ssrnres  5040  dmsnm  5063  coundi  5099  coundir  5100  cnvpom  5140  xpcom  5144  fun11  5249  fununi  5250  funcnvuni  5251  isarep1  5268  fsn  5651  fconstfvm  5697  eufnfv  5709  acexmidlem2  5833  eloprabga  5920  funoprabg  5932  ralrnmpo  5947  rexrnmpo  5948  oprabrexex2  6090  dfer2  6493  euen1b  6760  xpsnen  6778  rexuz3  10918  tgval2  12592  ssntr  12663  metrest  13047  sinhalfpilem  13253