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  696  pm4.15  699  3or6  1357  sbal1yz  2052  2exsb  2060  moanim  2152  2eu4  2171  cvjust  2224  abbi  2343  sbc8g  3036  ss2rab  3300  unass  3361  unss  3378  undi  3452  difindiss  3458  notm0  3512  disj  3540  unopab  4163  eqvinop  4330  pwexb  4566  dmun  4933  reldm0  4944  dmres  5029  imadmrn  5081  ssrnres  5174  dmsnm  5197  coundi  5233  coundir  5234  cnvpom  5274  xpcom  5278  fun11  5391  fununi  5392  funcnvuni  5393  isarep1  5410  fsn  5812  fconstfvm  5864  eufnfv  5877  acexmidlem2  6007  eloprabga  6100  funoprabg  6112  ralrnmpo  6128  rexrnmpo  6129  oprabrexex2  6284  dfer2  6694  euen1b  6968  xpsnen  6993  rexuz3  11522  imasaddfnlemg  13368  subsubrng2  14200  subsubrg2  14231  tgval2  14746  ssntr  14817  metrest  15201  plyun0  15431  sinhalfpilem  15486  2lgslem4  15803  wlkeq  16126  clwwlkn1  16186  clwwlkn2  16189