Theorem 3bitr4ri 212

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

Syntax hints:   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  dcnnOLD  835  excxor  1360  sbequ8  1827  2sb5  1963  2sb6  1964  2sb5rf  1969  2sb6rf  1970  moabs  2055  moanim  2080  2eu4  2099  2eu7  2100  sb8ab  2279  risset  2485  cbvreuvw  2686  reuind  2917  difundi  3359  indifdir  3363  unab  3374  inab  3375  rabeq0  3423  abeq0  3424  inssdif0im  3461  snprc  3624  snss  3685  unipr  3786  uni0b  3797  pwtr  4179  opm  4194  onintexmid  4531  elxp2  4603  opthprc  4636  xpiundir  4644  elvvv  4648  relun  4702  inopab  4717  difopab  4718  ralxpf  4731  rexxpf  4732  dmiun  4794  rniun  4995  cnvresima  5074  imaco  5090  fnopabg  5292  dff1o2  5418  idref  5704  imaiun  5707  opabex3d  6066  opabex3  6067  onntri35  7166  elixx3g  9798  elfz2  9912  elfzuzb  9915  divalgb  11808  1nprm  11982  alsconv  13619