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  768  orass  772  or32  775  dn1dc  966  an6  1355  excxor  1420  trubifal  1458  truxortru  1461  truxorfal  1462  falxortru  1463  falxorfal  1464  alrot4  1532  excom13  1735  sborv  1937  3exdistr  1962  4exdistr  1963  eeeanv  1984  ee4anv  1985  ee8anv  1986  sb3an  2009  sb9  2030  sbnf2  2032  sbco4  2058  2exsb  2060  sb8eu  2090  sb8euh  2100  sbmo  2137  2eu4  2171  2eu7  2172  elsb1  2207  elsb2  2208  r19.26-3  2661  rexcom13  2697  cbvreu  2763  ceqsex2  2841  ceqsex4v  2844  spc3gv  2896  ralrab2  2968  rexrab2  2970  reu2  2991  rmo4  2996  reu8  2999  rmo3f  3000  sbc3an  3090  reu8nf  3110  rmo3  3121  ssalel  3212  ss2rab  3300  rabss  3301  ssrab  3302  dfdif3  3314  undi  3452  undif3ss  3465  difin2  3466  dfnul2  3493  disj  3540  disjsn  3728  snssb  3801  uni0c  3914  ssint  3939  iunss  4006  ssextss  4306  eqvinop  4329  opcom  4337  opeqsn  4339  opeqpr  4340  brabsb  4349  opelopabf  4363  opabm  4369  pofun  4403  sotritrieq  4416  uniuni  4542  ordsucim  4592  opeliunxp  4774  xpiundi  4777  brinxp2  4786  ssrel  4807  reliun  4840  cnvuni  4908  dmopab3  4936  opelres  5010  elres  5041  elsnres  5042  intirr  5115  ssrnres  5171  dminxp  5173  dfrel4v  5180  dmsnm  5194  rnco  5235  sb8iota  5286  dffun2  5328  dffun4f  5334  funco  5358  funcnveq  5384  fun11  5388  isarep1  5407  dff1o4  5582  dff1o6  5906  oprabid  6039  mpo2eqb  6120  ralrnmpo  6125  rexrnmpo  6126  opabex3d  6272  opabex3  6273  xporderlem  6383  f1od2  6387  tfr0dm  6474  tfrexlem  6486  frec0g  6549  nnaord  6663  ecid  6753  mptelixpg  6889  elixpsn  6890  mapsnen  6972  xpsnen  6988  xpcomco  6993  xpassen  6997  exmidontriimlem3  7413  nqnq0  7636  opelreal  8022  pitoregt0  8044  elnn0  9379  elxnn0  9442  elxr  9980  xrnepnf  9982  elfzuzb  10223  4fvwrd4  10344  elfzo2  10354  swrdnd  11199  resqrexlemsqa  11543  fisumcom2  11957  modfsummod  11977  fprodcom2fi  12145  nnwosdc  12568  isprm2  12647  isprm4  12649  pythagtriplem2  12797  4sqlem12  12933  isnsg2  13748  isnsg4  13757  dfrhm2  14126  cnfldui  14561  ntreq0  14814  txbas  14940  metrest  15188  2lgslem4  15790  umgr2edg1  16015