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  854  excxor  1420  sbequ8  1893  2sb5  2034  2sb6  2035  2sb5rf  2040  2sb6rf  2041  moabs  2127  moanim  2152  2eu4  2171  2eu7  2172  sb8ab  2351  risset  2558  cbvreuvw  2771  reuind  3008  difundi  3456  indifdir  3460  unab  3471  inab  3472  rabeq0  3521  abeq0  3522  inssdif0im  3559  snprc  3731  snssOLD  3794  unipr  3902  uni0b  3913  pwtr  4306  opm  4321  onintexmid  4666  elxp2  4738  opthprc  4772  xpiundir  4780  elvvv  4784  relun  4839  inopab  4857  difopab  4858  ralxpf  4871  rexxpf  4872  dmiun  4935  rniun  5142  cnvresima  5221  imaco  5237  fnopabg  5450  dff1o2  5582  idref  5889  imaiun  5893  opabex3d  6275  opabex3  6276  onntri35  7438  elixx3g  10114  elfz2  10228  elfzuzb  10232  divalgb  12457  1nprm  12657  issubg3  13750  cnfldui  14574  alsconv  16562