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  680  orass  684  or32  687  dcan  842  dn1dc  867  an6  1216  excxor  1269  trubifal  1307  truxortru  1310  truxorfal  1311  falxortru  1312  falxorfal  1313  alrot4  1375  excom13  1579  sborv  1770  3exdistr  1792  4exdistr  1793  eeeanv  1808  ee4anv  1809  ee8anv  1810  sb3an  1832  elsb3  1852  elsb4  1853  sb9  1855  sbnf2  1857  sbco4  1883  2exsb  1885  sb8eu  1913  sb8euh  1923  sbmo  1959  2eu4  1993  2eu7  1994  r19.26-3  2443  rexcom13  2475  cbvreu  2531  ceqsex2  2594  ceqsex4v  2597  spc3gv  2645  ralrab2  2706  rexrab2  2708  reu2  2729  rmo4  2734  reu8  2737  rmo3  2849  dfss2  2934  ss2rab  3016  rabss  3017  ssrab  3018  undi  3185  undif3ss  3198  difin2  3199  dfnul2  3226  disj  3268  disjsn  3432  uni0c  3606  ssint  3631  iunss  3698  ssextss  3956  eqvinop  3980  opcom  3987  opeqsn  3989  opeqpr  3990  brabsb  3998  opelopabf  4011  opabm  4017  pofun  4049  sotritrieq  4062  uniuni  4183  ordsucim  4226  opeliunxp  4395  xpiundi  4398  brinxp2  4407  ssrel  4428  reliun  4458  cnvuni  4521  dmopab3  4548  opelres  4617  elres  4646  elsnres  4647  intirr  4711  ssrnres  4763  dminxp  4765  dfrel4v  4772  dmsnm  4786  rnco  4827  sb8iota  4874  dffun2  4912  dffun4f  4918  funco  4940  funcnveq  4962  fun11  4966  isarep1  4985  dff1o4  5134  dff1o6  5416  oprabid  5537  mpt22eqb  5610  ralrnmpt2  5615  rexrnmpt2  5616  opabex3d  5748  opabex3  5749  xporderlem  5852  tfr0  5937  tfrexlem  5948  frec0g  5983  nnaord  6082  ecid  6169  xpsnen  6295  xpcomco  6300  xpassen  6304  nqnq0  6539  opelreal  6904  pitoregt0  6925  elnn0  8183  elxr  8696  xrnepnf  8700  elfzuzb  8884  4fvwrd4  8997  elfzo2  9007  resqrexlemsqa  9622