Theorem 3bitri 206

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 184	. 2 ⊢ (𝜓 ↔ 𝜃)
5	1, 4	bitri 184	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:  bibi1i  228  an32  562  orbi1i  765  orass  769  or32  772  dn1dc  963  an6  1334  excxor  1398  trubifal  1436  truxortru  1439  truxorfal  1440  falxortru  1441  falxorfal  1442  alrot4  1510  excom13  1713  sborv  1915  3exdistr  1940  4exdistr  1941  eeeanv  1962  ee4anv  1963  ee8anv  1964  sb3an  1987  sb9  2008  sbnf2  2010  sbco4  2036  2exsb  2038  sb8eu  2068  sb8euh  2078  sbmo  2114  2eu4  2148  2eu7  2149  elsb1  2184  elsb2  2185  r19.26-3  2637  rexcom13  2673  cbvreu  2737  ceqsex2  2815  ceqsex4v  2818  spc3gv  2870  ralrab2  2942  rexrab2  2944  reu2  2965  rmo4  2970  reu8  2973  rmo3f  2974  sbc3an  3064  rmo3  3094  ssalel  3185  ss2rab  3273  rabss  3274  ssrab  3275  dfdif3  3287  undi  3425  undif3ss  3438  difin2  3439  dfnul2  3466  disj  3513  disjsn  3699  snssb  3771  uni0c  3881  ssint  3906  iunss  3973  ssextss  4271  eqvinop  4294  opcom  4302  opeqsn  4304  opeqpr  4305  brabsb  4314  opelopabf  4328  opabm  4334  pofun  4366  sotritrieq  4379  uniuni  4505  ordsucim  4555  opeliunxp  4737  xpiundi  4740  brinxp2  4749  ssrel  4770  reliun  4803  cnvuni  4871  dmopab3  4899  opelres  4972  elres  5003  elsnres  5004  intirr  5077  ssrnres  5133  dminxp  5135  dfrel4v  5142  dmsnm  5156  rnco  5197  sb8iota  5247  dffun2  5289  dffun4f  5295  funco  5319  funcnveq  5345  fun11  5349  isarep1  5368  dff1o4  5541  dff1o6  5857  oprabid  5988  mpo2eqb  6067  ralrnmpo  6072  rexrnmpo  6073  opabex3d  6218  opabex3  6219  xporderlem  6329  f1od2  6333  tfr0dm  6420  tfrexlem  6432  frec0g  6495  nnaord  6607  ecid  6697  mptelixpg  6833  elixpsn  6834  mapsnen  6916  xpsnen  6930  xpcomco  6935  xpassen  6939  exmidontriimlem3  7350  nqnq0  7569  opelreal  7955  pitoregt0  7977  elnn0  9312  elxnn0  9375  elxr  9913  xrnepnf  9915  elfzuzb  10156  4fvwrd4  10277  elfzo2  10287  swrdnd  11130  resqrexlemsqa  11405  fisumcom2  11819  modfsummod  11839  fprodcom2fi  12007  nnwosdc  12430  isprm2  12509  isprm4  12511  pythagtriplem2  12659  4sqlem12  12795  isnsg2  13609  isnsg4  13618  dfrhm2  13986  cnfldui  14421  ntreq0  14674  txbas  14800  metrest  15048  2lgslem4  15650