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  3053  ss2rab  3318  unass  3380  unss  3397  undi  3473  difindiss  3479  notm0  3533  disj  3561  unopab  4194  eqvinop  4364  pwexb  4600  dmun  4968  reldm0  4979  dmres  5064  imadmrn  5116  ssrnres  5210  dmsnm  5233  coundi  5269  coundir  5270  cnvpom  5310  xpcom  5314  fun11  5428  fununi  5429  funcnvuni  5430  isarep1  5447  fsn  5854  fconstfvm  5907  eufnfv  5922  fdmrn  6007  acexmidlem2  6055  eloprabga  6148  funoprabg  6160  ralrnmpo  6176  rexrnmpo  6177  oprabrexex2  6336  dfer2  6781  euen1b  7056  xpsnen  7085  rexuz3  11703  ballotfilem2  13175  ballotfilemi1  13192  imasaddfnlemg  13581  subsubrng2  14464  subsubrg2  14495  tgval2  15045  ssntr  15116  metrest  15500  plyun0  15730  sinhalfpilem  15785  2lgslem4  16105  wlkeq  16478  clwwlkn1  16542  clwwlkn2  16545  clwwlknon2x  16559