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  699  pm4.15  702  3or6  1360  sbal1yz  2057  2exsb  2065  moanim  2157  2eu4  2176  cvjust  2229  abbibcom  2348  sbc8g  3052  ss2rab  3316  unass  3378  unss  3395  undi  3471  difindiss  3477  notm0  3531  disj  3559  unopab  4191  eqvinop  4361  pwexb  4597  dmun  4965  reldm0  4976  dmres  5061  imadmrn  5113  ssrnres  5207  dmsnm  5230  coundi  5266  coundir  5267  cnvpom  5307  xpcom  5311  fun11  5425  fununi  5426  funcnvuni  5427  isarep1  5444  fsn  5851  fconstfvm  5904  eufnfv  5919  acexmidlem2  6049  eloprabga  6142  funoprabg  6154  ralrnmpo  6170  rexrnmpo  6171  oprabrexex2  6325  dfer2  6770  euen1b  7045  xpsnen  7074  rexuz3  11683  ballotfilem2  13153  imasaddfnlemg  13548  subsubrng2  14383  subsubrg2  14414  tgval2  14965  ssntr  15036  metrest  15420  plyun0  15650  sinhalfpilem  15705  2lgslem4  16025  wlkeq  16398  clwwlkn1  16462  clwwlkn2  16465  clwwlknon2x  16479