Theorem 3bitr2ri 291

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)

Hypotheses

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

Assertion

Ref	Expression
3bitr2ri	⊢ (𝜃 ↔ 𝜑)

Proof of Theorem 3bitr2ri

Step	Hyp	Ref	Expression
1		3bitr2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		3bitr2i.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	1, 2	bitr4i 269	. 2 ⊢ (𝜑 ↔ 𝜒)
4		3bitr2i.3	. 2 ⊢ (𝜒 ↔ 𝜃)
5	3, 4	bitr2i 267	1 ⊢ (𝜃 ↔ 𝜑)

Syntax hints:   ↔ wb 197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 198

This theorem is referenced by:  xorass  1637  ssrab  3840  copsex2gb  5398  relop  5441  dmopab3  5505  dfres2  5630  restidsing  5642  idrefOLD  5692  fununi  6142  dffv2  6460  dfsup2  8557  kmlem3  9227  recmulnq  10039  nbgrel  26512  shne0i  28698  ssiun3  29759  cnvoprabOLD  29882  ind1a  30463  bnj1304  31270  bnj1253  31465  dmscut  32294  dfrecs2  32433  icorempt2  33564  inxprnres  34424  dalem20  35581  rp-isfinite6  38471  rababg  38486  ssrabf  39880