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  496  orbi1i  679  orass  683  or32  686  dcan  841  dn1dc  866  an6  1215  excxor  1268  trubifal  1304  truxortru  1307  truxorfal  1308  falxortru  1309  falxorfal  1310  alrot4  1372  excom13  1576  sborv  1767  3exdistr  1789  4exdistr  1790  eeeanv  1805  ee4anv  1806  ee8anv  1807  sb3an  1829  elsb3  1849  elsb4  1850  sb9  1852  sbnf2  1854  sbco4  1880  2exsb  1882  sb8eu  1910  sb8euh  1920  sbmo  1956  2eu4  1990  2eu7  1991  r19.26-3  2437  rexcom13  2469  cbvreu  2525  ceqsex2  2588  ceqsex4v  2591  spc3gv  2639  ralrab2  2700  rexrab2  2702  reu2  2723  rmo4  2728  reu8  2731  rmo3  2843  dfss2  2928  ss2rab  3010  rabss  3011  ssrab  3012  undi  3179  undif3ss  3192  difin2  3193  dfnul2  3220  disj  3262  disjsn  3423  uni0c  3597  ssint  3622  iunss  3689  ssextss  3947  eqvinop  3971  opcom  3978  opeqsn  3980  opeqpr  3981  brabsb  3989  opelopabf  4002  opabm  4008  pofun  4040  sotritrieq  4053  uniuni  4149  ordsucim  4192  opeliunxp  4338  xpiundi  4341  brinxp2  4350  ssrel  4371  reliun  4401  cnvuni  4464  dmopab3  4491  opelres  4560  elres  4589  elsnres  4590  intirr  4654  ssrnres  4706  dminxp  4708  dfrel4v  4715  dmsnm  4729  rnco  4770  sb8iota  4817  dffun2  4855  dffun4f  4861  funco  4883  funcnveq  4905  fun11  4909  isarep1  4928  dff1o4  5077  dff1o6  5359  oprabid  5480  mpt22eqb  5552  ralrnmpt2  5557  rexrnmpt2  5558  opabex3d  5690  opabex3  5691  xporderlem  5793  tfr0  5878  tfrexlem  5889  frec0g  5922  nnaord  6018  ecid  6105  xpsnen  6231  xpcomco  6236  xpassen  6240  nqnq0  6424  opelreal  6726  elnn0  7959  elxr  8466  xrnepnf  8470  elfzuzb  8654  4fvwrd4  8767  elfzo2  8777