Theorem 3bitr4ri 213

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)

Hypotheses

Ref	Expression
3bitr4i.1	⊢ (𝜑 ↔ 𝜓)
3bitr4i.2	⊢ (𝜒 ↔ 𝜑)
3bitr4i.3	⊢ (𝜃 ↔ 𝜓)

Assertion

Ref	Expression
3bitr4ri	⊢ (𝜃 ↔ 𝜒)

Proof of Theorem 3bitr4ri

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 ⊢ (𝜒 ↔ 𝜑)
2		3bitr4i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		3bitr4i.3	. . 3 ⊢ (𝜃 ↔ 𝜓)
4	2, 3	bitr4i 187	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitr2i 185	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:  dcnnOLD  849  excxor  1378  sbequ8  1847  2sb5  1983  2sb6  1984  2sb5rf  1989  2sb6rf  1990  moabs  2075  moanim  2100  2eu4  2119  2eu7  2120  sb8ab  2299  risset  2505  cbvreuvw  2711  reuind  2944  difundi  3389  indifdir  3393  unab  3404  inab  3405  rabeq0  3454  abeq0  3455  inssdif0im  3492  snprc  3659  snssOLD  3720  unipr  3825  uni0b  3836  pwtr  4221  opm  4236  onintexmid  4574  elxp2  4646  opthprc  4679  xpiundir  4687  elvvv  4691  relun  4745  inopab  4761  difopab  4762  ralxpf  4775  rexxpf  4776  dmiun  4838  rniun  5041  cnvresima  5120  imaco  5136  fnopabg  5341  dff1o2  5468  idref  5760  imaiun  5764  opabex3d  6125  opabex3  6126  onntri35  7239  elixx3g  9904  elfz2  10018  elfzuzb  10022  divalgb  11933  1nprm  12117  issubg3  13062  alsconv  14990