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  698  3or6  1338  sbal1yz  2032  2exsb  2040  moanim  2132  2eu4  2151  cvjust  2204  abbi  2323  sbc8g  3016  ss2rab  3280  unass  3341  unss  3358  undi  3432  difindiss  3438  notm0  3492  disj  3520  unopab  4142  eqvinop  4308  pwexb  4542  dmun  4907  reldm0  4918  dmres  5002  imadmrn  5054  ssrnres  5147  dmsnm  5170  coundi  5206  coundir  5207  cnvpom  5247  xpcom  5251  fun11  5364  fununi  5365  funcnvuni  5366  isarep1  5383  fsn  5780  fconstfvm  5830  eufnfv  5843  acexmidlem2  5971  eloprabga  6062  funoprabg  6074  ralrnmpo  6090  rexrnmpo  6091  oprabrexex2  6245  dfer2  6651  euen1b  6925  xpsnen  6948  rexuz3  11467  imasaddfnlemg  13313  subsubrng2  14144  subsubrg2  14175  tgval2  14690  ssntr  14761  metrest  15145  plyun0  15375  sinhalfpilem  15430  2lgslem4  15747