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  698  pm4.15  701  3or6  1359  sbal1yz  2053  2exsb  2061  moanim  2153  2eu4  2172  cvjust  2225  abbi  2344  sbc8g  3038  ss2rab  3302  unass  3363  unss  3380  undi  3454  difindiss  3460  notm0  3514  disj  3542  unopab  4169  eqvinop  4337  pwexb  4573  dmun  4940  reldm0  4951  dmres  5036  imadmrn  5088  ssrnres  5181  dmsnm  5204  coundi  5240  coundir  5241  cnvpom  5281  xpcom  5285  fun11  5399  fununi  5400  funcnvuni  5401  isarep1  5418  fsn  5822  fconstfvm  5875  eufnfv  5890  acexmidlem2  6020  eloprabga  6113  funoprabg  6125  ralrnmpo  6141  rexrnmpo  6142  oprabrexex2  6297  dfer2  6708  euen1b  6982  xpsnen  7010  rexuz3  11573  imasaddfnlemg  13420  subsubrng2  14253  subsubrg2  14284  tgval2  14804  ssntr  14875  metrest  15259  plyun0  15489  sinhalfpilem  15544  2lgslem4  15861  wlkeq  16234  clwwlkn1  16298  clwwlkn2  16301  clwwlknon2x  16315