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  850  excxor  1389  sbequ8  1861  2sb5  2002  2sb6  2003  2sb5rf  2008  2sb6rf  2009  moabs  2094  moanim  2119  2eu4  2138  2eu7  2139  sb8ab  2318  risset  2525  cbvreuvw  2735  reuind  2969  difundi  3415  indifdir  3419  unab  3430  inab  3431  rabeq0  3480  abeq0  3481  inssdif0im  3518  snprc  3687  snssOLD  3748  unipr  3853  uni0b  3864  pwtr  4252  opm  4267  onintexmid  4609  elxp2  4681  opthprc  4714  xpiundir  4722  elvvv  4726  relun  4780  inopab  4798  difopab  4799  ralxpf  4812  rexxpf  4813  dmiun  4875  rniun  5080  cnvresima  5159  imaco  5175  fnopabg  5381  dff1o2  5509  idref  5803  imaiun  5807  opabex3d  6178  opabex3  6179  onntri35  7304  elixx3g  9976  elfz2  10090  elfzuzb  10094  divalgb  12090  1nprm  12282  issubg3  13322  cnfldui  14145  alsconv  15724