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  1999  2exsb  2007  moanim  2098  2eu4  2117  cvjust  2170  abbi  2289  sbc8g  2968  ss2rab  3229  unass  3290  unss  3307  undi  3381  difindiss  3387  notm0  3441  disj  3469  unopab  4077  eqvinop  4237  pwexb  4468  dmun  4827  reldm0  4838  dmres  4921  imadmrn  4973  ssrnres  5063  dmsnm  5086  coundi  5122  coundir  5123  cnvpom  5163  xpcom  5167  fun11  5275  fununi  5276  funcnvuni  5277  isarep1  5294  fsn  5680  fconstfvm  5726  eufnfv  5738  acexmidlem2  5862  eloprabga  5952  funoprabg  5964  ralrnmpo  5979  rexrnmpo  5980  oprabrexex2  6121  dfer2  6526  euen1b  6793  xpsnen  6811  rexuz3  10965  tgval2  13120  ssntr  13191  metrest  13575  sinhalfpilem  13781