Theorem 3bitri 205

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 183	. 2 ⊢ (𝜓 ↔ 𝜃)
5	1, 4	bitri 183	1 ⊢ (𝜑 ↔ 𝜃)

Syntax hints:   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bibi1i  227  an32  551  orbi1i  752  orass  756  or32  759  dcan  918  dn1dc  944  an6  1299  excxor  1356  trubifal  1394  truxortru  1397  truxorfal  1398  falxortru  1399  falxorfal  1400  alrot4  1462  excom13  1667  sborv  1862  3exdistr  1887  4exdistr  1888  eeeanv  1903  ee4anv  1904  ee8anv  1905  sb3an  1929  elsb3  1949  elsb4  1950  sb9  1952  sbnf2  1954  sbco4  1980  2exsb  1982  sb8eu  2010  sb8euh  2020  sbmo  2056  2eu4  2090  2eu7  2091  r19.26-3  2560  rexcom13  2594  cbvreu  2650  ceqsex2  2721  ceqsex4v  2724  spc3gv  2773  ralrab2  2844  rexrab2  2846  reu2  2867  rmo4  2872  reu8  2875  rmo3f  2876  sbc3an  2965  rmo3  2995  dfss2  3081  ss2rab  3168  rabss  3169  ssrab  3170  dfdif3  3181  undi  3319  undif3ss  3332  difin2  3333  dfnul2  3360  disj  3406  disjsn  3580  uni0c  3757  ssint  3782  iunss  3849  ssextss  4137  eqvinop  4160  opcom  4167  opeqsn  4169  opeqpr  4170  brabsb  4178  opelopabf  4191  opabm  4197  pofun  4229  sotritrieq  4242  uniuni  4367  ordsucim  4411  opeliunxp  4589  xpiundi  4592  brinxp2  4601  ssrel  4622  reliun  4655  cnvuni  4720  dmopab3  4747  opelres  4819  elres  4850  elsnres  4851  intirr  4920  ssrnres  4976  dminxp  4978  dfrel4v  4985  dmsnm  4999  rnco  5040  sb8iota  5090  dffun2  5128  dffun4f  5134  funco  5158  funcnveq  5181  fun11  5185  isarep1  5204  dff1o4  5368  dff1o6  5670  oprabid  5796  mpo2eqb  5873  ralrnmpo  5878  rexrnmpo  5879  opabex3d  6012  opabex3  6013  xporderlem  6121  f1od2  6125  tfr0dm  6212  tfrexlem  6224  frec0g  6287  nnaord  6398  ecid  6485  mptelixpg  6621  elixpsn  6622  mapsnen  6698  xpsnen  6708  xpcomco  6713  xpassen  6717  nqnq0  7242  opelreal  7628  pitoregt0  7650  elnn0  8972  elxnn0  9035  elxr  9556  xrnepnf  9558  elfzuzb  9793  4fvwrd4  9910  elfzo2  9920  resqrexlemsqa  10789  fisumcom2  11200  modfsummod  11220  isprm2  11787  isprm4  11789  ntreq0  12290  txbas  12416  metrest  12664