Theorem 3bitri 195

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
3bitri.1	⊢ (φ ↔ ψ)
3bitri.2	⊢ (ψ ↔ χ)
3bitri.3	⊢ (χ ↔ θ)

Assertion

Ref	Expression
3bitri	⊢ (φ ↔ θ)

Proof of Theorem 3bitri

Step	Hyp	Ref	Expression
1		3bitri.1	. 2 ⊢ (φ ↔ ψ)
2		3bitri.2	. . 3 ⊢ (ψ ↔ χ)
3		3bitri.3	. . 3 ⊢ (χ ↔ θ)
4	2, 3	bitri 173	. 2 ⊢ (ψ ↔ θ)
5	1, 4	bitri 173	1 ⊢ (φ ↔ θ)

Syntax hints:   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  bibi1i  217  an32  481  orbi1i  664  orass  668  or32  671  dcan  824  dn1dc  849  an6  1197  excxor  1250  trubifal  1286  truxortru  1289  truxorfal  1290  falxortru  1291  falxorfal  1292  alrot4  1349  excom13  1553  sborv  1744  3exdistr  1766  4exdistr  1767  eeeanv  1782  ee4anv  1783  ee8anv  1784  sb3an  1806  elsb3  1826  elsb4  1827  sb9  1829  sbnf2  1831  sbco4  1857  2exsb  1859  sb8eu  1887  sb8euh  1897  sbmo  1933  2eu4  1967  2eu7  1968  r19.26-3  2413  rexcom13  2445  cbvreu  2501  ceqsex2  2563  ceqsex4v  2566  spc3gv  2614  ralrab2  2675  rexrab2  2677  reu2  2698  rmo4  2703  reu8  2706  rmo3  2818  dfss2  2903  ss2rab  2985  rabss  2986  ssrab  2987  undi  3154  undif3ss  3167  difin2  3168  dfnul2  3195  disj  3237  disjsn  3396  uni0c  3570  ssint  3595  iunss  3662  ssextss  3920  eqvinop  3944  opcom  3951  opeqsn  3953  opeqpr  3954  brabsb  3962  opelopabf  3975  opabm  3981  pofun  4013  sotritrieq  4026  uniuni  4122  ordsucim  4165  opeliunxp  4311  xpiundi  4314  brinxp2  4323  ssrel  4344  reliun  4374  cnvuni  4437  dmopab3  4464  opelres  4533  elres  4562  elsnres  4563  intirr  4627  ssrnres  4679  dminxp  4681  dfrel4v  4688  dmsnm  4702  rnco  4743  sb8iota  4790  dffun2  4828  dffun4f  4833  funco  4855  funcnveq  4877  fun11  4881  isarep1  4900  dff1o4  5048  dff1o6  5330  oprabid  5450  mpt22eqb  5522  ralrnmpt2  5527  rexrnmpt2  5528  opabex3d  5660  opabex3  5661  xporderlem  5763  tfrexlem  5859  frec0g  5891  nnaord  5982  ecid  6069  nqnq0  6283  opelreal  6536  elnn0  7758  elxr  8173  xrnepnf  8177