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  857  excxor  1423  sbequ8  1896  2sb5  2039  2sb6  2040  2sb5rf  2045  2sb6rf  2046  moabs  2132  moanim  2157  2eu4  2176  2eu7  2177  sb8ab  2358  risset  2572  cbvreuvw  2786  reuind  3025  difundi  3477  indifdir  3481  unab  3492  inab  3493  rabeq0  3542  abeq0  3543  inssdif0im  3580  snprc  3759  snssOLD  3824  unipr  3933  uni0b  3944  pwtr  4340  opm  4355  onintexmid  4700  elxp2  4772  opthprc  4806  xpiundir  4814  elvvv  4818  relun  4874  inopab  4892  difopab  4893  ralxpf  4906  rexxpf  4907  dmiun  4970  rniun  5178  cnvresima  5257  imaco  5273  fnopabg  5487  dff1o2  5624  idref  5935  imaiun  5939  opabex3d  6323  opabex3  6324  onntri35  7560  elixx3g  10253  elfz2  10368  elfzuzb  10372  divalgb  12636  1nprm  12836  issubg3  13993  cnfldui  14849  alsconv  16989