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 ⊢ (𝜒 ↔ 𝜑)

This proof depends on syntax axioms:   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3bitrri  207  3bitr2ri  209  3bitr4ri  213  nan  703  pm4.15  706  3or6  1364  sbal1yz  2061  2exsb  2069  moanim  2161  2eu4  2180  cvjust  2233  abbibcom  2352  sbc8g  3059  ss2rab  3324  unass  3386  unss  3403  undi  3479  difindiss  3485  notm0  3542  disj  3573  unopab  4211  eqvinop  4385  pwexb  4622  dmun  4990  reldm0  5001  dmres  5086  imadmrn  5139  ssrnres  5233  dmsnm  5256  coundi  5292  coundir  5293  cnvpom  5333  xpcom  5337  fun11  5451  fununi  5452  funcnvuni  5453  isarep1  5470  fsn  5883  fconstfvm  5936  eufnfv  5952  fdmrn  6037  acexmidlem2  6085  eloprabga  6178  funoprabg  6190  ralrnmpo  6206  rexrnmpo  6207  oprabrexex2  6367  dfer2  6812  euen1b  7095  xpsnen  7124  rexuz3  11779  ballotfilem2  13287  ballotfilemi1  13304  imasaddfnlemg  13695  subsubrng2  14633  subsubrg2  14664  tgval2  15289  ssntr  15360  metrest  15744  plyun0  15974  sinhalfpilem  16030  2lgslem4  16439  wlkeq  16812  clwwlkn1  16876  clwwlkn2  16879  clwwlknon2x  16893