Theorem 3bitr2ri 303

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 281	. 2 ⊢ (𝜑 ↔ 𝜒)
4		3bitr2i.3	. 2 ⊢ (𝜒 ↔ 𝜃)
5	3, 4	bitr2i 279	1 ⊢ (𝜃 ↔ 𝜑)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  xorass  1538  ssrab  4027  copsex2gb  5783  relop  5826  dmopab3  5899  rnopab3  5936  dfres2  6033  restidsing  6045  fununi  6600  dffv2  6966  dfsup2  9392  kmlem3  10124  recmulnq  10937  ind1a  12217  dmcuts  27938  nbgrel  29595  shne0i  31705  13an22anass  32717  ssiun3  32809  bnj1304  35119  bnj1253  35317  dfrecs2  36308  icorempo  37852  inxprnres  38804  disjressuc2  38917  dalem20  40324  ralopabb  43994  rp-isfinite6  44101  rababg  44157  nregmodel  45585  ssrabf  45691  ralfal  45738