Theorem 3bitri 296

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-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 274	. 2 ⊢ (𝜓 ↔ 𝜃)
5	1, 4	bitri 274	1 ⊢ (𝜑 ↔ 𝜃)

Syntax hints:   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  bibi1i  338  pm5.32  574  biadan  816  orbi1i  911  orass  919  or32  923  cases  1040  dn1  1055  3anidm  1103  an3andi  1481  an33rean  1482  an33reanOLD  1483  nanbi  1495  excxor  1512  cadan  1607  cadcomb  1611  nic-axALT  1673  tbw-bijust  1697  rb-bijust  1748  nf2  1784  19.43  1882  19.43OLD  1883  3exdistr  1961  19.12vvv  1989  sbcom2  2158  excom13  2161  sbco4  2272  sbn  2274  19.12vv  2342  eeeanv  2345  ee4anv  2346  2sb8ef  2351  sbel2x  2471  2sb8e  2532  dfmo  2593  sb8eulem  2595  2mo2  2646  2eu7  2656  2eu8  2657  sbabel  2937  r19.26-3  3110  r19.23v  3174  2ralor  3214  rexcomOLD  3269  ralcom13OLD  3273  rexcom13  3274  cbvreuwOLD  3395  cbvreu  3399  ceqsralt  3467  ceqsalv  3471  ceqsex2  3486  ceqsex2v  3487  ceqsex4v  3489  ralrab2  3639  rexrab2  3641  reu2  3664  rmo4  3669  reu8  3672  rmo3f  3673  2reu5lem3  3696  sbc3an  3790  sbcimdv  3794  reu8nf  3814  rmo2  3824  rmo3  3826  rmoanim  3831  dfss2OLD  3912  ss2rab  4009  rabss  4010  ssrab  4011  dfdif3  4054  symdifass  4190  dfss4  4197  undi  4213  indifdi  4222  undif3  4229  difin2  4230  difin0ss  4307  ab0OLD  4314  disj  4386  disjOLD  4387  disj4  4397  rabsssn  4606  disjsn  4650  snssb  4721  raldifsni  4733  ssunpr  4770  sspr  4771  sstp  4772  uni0b  4872  uni0c  4873  ssint  4901  intprg  4918  iunssf  4980  iunss  4981  iundif2  5009  disjor  5060  nfnid  5306  reusv2lem4  5332  ssextss  5381  exss  5390  eqvinop  5413  sbcop  5415  opcom  5427  opeqpr  5431  brtp  5449  brabsb  5457  opelopabf  5471  dfid3  5503  pofun  5532  opeliunxp  5665  xpiundi  5668  brinxp2  5675  reliun  5738  exopxfr  5765  cnvuni  5808  dmopab3  5841  rnep  5848  elres  5942  elsnres  5943  elrid  5965  cnvsym  6032  cnvsymOLD  6033  asymref2  6037  intirr  6038  xpeq0  6078  xpdifid  6086  ssrnres  6096  dminxp  6098  dfrel4v  6108  elid  6117  dmsnn0  6125  rnco  6170  coeq0  6173  resssxp  6188  dfpo2  6214  sspred  6226  frpoind  6260  wfiOLD  6269  sb8iota  6422  dffun2OLDOLD  6470  fun11  6537  isarep1  6552  isarep1OLD  6553  dff1o4  6754  opabiota  6883  fvopab5  6939  eqfnfv3  6943  fvn0ssdmfun  6984  fnressn  7062  f13dfv  7178  dff1o6  7179  fliftel  7212  oprabidw  7339  oprabid  7340  eloprabga  7415  mpo2eqb  7439  ralrnmpo  7445  uniuni  7645  dflim3  7730  dfom2  7750  elxp4  7805  elxp5  7806  opabex3d  7844  opabex3rd  7845  opabex3  7846  el2xptp  7913  fsplit  7993  xporderlem  8003  dfrecs3  8238  dfrecs3OLD  8239  tz7.48lem  8307  seqomlem2  8317  oaord  8414  oeeu  8470  nnaord  8486  ecid  8607  mptelixpg  8759  elixpsn  8761  xpsnen  8885  xpcomco  8892  xpassen  8896  omxpenlem  8903  dom0OLD  8933  modom  9074  brttrcl2  9530  ttrcltr  9532  rnttrcl  9538  frind  9566  tz9.12lem3  9605  rankxpsuc  9698  cp  9707  cardprclem  9795  infxpenlem  9829  dfac5lem1  9939  dfac5lem2  9940  dfac5lem5  9943  dfac10c  9954  kmlem3  9968  kmlem12  9977  kmlem13  9978  kmlem14  9979  kmlem15  9980  ackbij2  10059  cf0  10067  cflim2  10079  dffin7-2  10214  dfacfin7  10215  fin1a2lem12  10227  axdc3lem3  10268  cfpwsdom  10400  recmulnq  10780  genpass  10825  psslinpr  10847  suplem2pr  10869  opelreal  10946  ltxrlt  11105  addid1  11215  elnn0  12295  elxnn0  12367  elnn0z  12392  nnwos  12715  elxr  12912  xrnepnf  12914  elfzuzb  13310  4fvwrd4  13436  preduz  13438  elfzo2  13450  ssnn0fi  13765  sqeqori  13990  xpcogend  14744  cotr2g  14746  fsumcom2  15545  modfsummod  15565  fprodcom2  15753  rpnnen2lem12  15993  gcdcllem1  16265  isprm2  16446  isprm7  16472  pythagtriplem2  16577  infpn2  16673  4sqlem12  16716  initoid  17775  termoid  17776  eldmcoa  17839  oduposb  18106  gsumwspan  18544  smndex1basss  18603  smndex1mgm  18605  isnsg2  18843  isnsg4  18854  cycsubmel  18878  efgcpbllemb  19420  dmdprd  19660  dprdval  19665  dprdw  19672  dprd2d2  19706  dfrhm2  20020  brric2  20048  issubrg  20087  islmim  20387  lbsextlem2  20484  cnfldfun  20672  pjfval2  20979  opsrtoslem1  21325  ntreq0  22291  cmpcov2  22604  cmpsub  22614  2ndcdisj  22670  unisngl  22741  txbas  22781  elpt  22786  txkgen  22866  xkococn  22874  fbun  23054  trfil2  23101  fin1aufil  23146  alexsubALTlem3  23263  cnextcn  23281  qustgplem  23335  eltsms  23347  ustn0  23435  fmucndlem  23506  metrest  23743  restmetu  23789  isclmp  24323  srabn  24587  ellogdm  25857  1cubr  26055  leibpilem2  26154  dmarea  26170  vmasum  26427  dchrelbas2  26448  2lgslem4  26617  tgcgr4  26990  ltgov  27056  axlowdimlem13  27420  axeuclidlem  27428  numedglnl  27612  nbupgrres  27829  vtxd0nedgb  27953  rusgrprc  28055  usgr2pth0  28231  wspthsnwspthsnon  28379  isclwwlk  28446  clwwlkn1  28503  clwwlkn2  28506  clwwlknonel  28557  3pthdlem1  28626  iseupthf1o  28664  frgr3v  28737  fusgr2wsp2nb  28796  frgrregord013  28857  h2hcau  29439  h2hlm  29440  shlesb1i  29846  shne0i  29908  chnlei  29945  cmbr2i  30056  pjneli  30183  ho02i  30289  adjsym  30293  adjeu  30349  lnopeqi  30468  largei  30727  atoml2i  30843  cdj3lem3b  30900  or3di  30908  mo5f  30935  dmrab  30942  disjnf  31007  disjorf  31016  ssrelf  31053  ofpreima  31100  disjdsct  31133  1stpreima  31137  2ndpreima  31138  f1od2  31154  xrdifh  31199  nndiffz1  31205  prmidl0  31721  zarclsun  31916  ordtconnlem1  31970  ind1a  32083  measiuns  32281  elunirnmbfm  32316  eulerpartlemr  32437  eulerpartlemgh  32441  eulerpartlemn  32444  ballotlemodife  32560  bnj250  32776  bnj334  32788  bnj345  32789  bnj89  32796  bnj115  32800  bnj919  32843  bnj1304  32895  bnj92  32938  bnj124  32947  bnj126  32949  bnj154  32954  bnj155  32955  bnj523  32963  bnj526  32964  bnj540  32968  bnj581  32984  bnj916  33009  bnj929  33012  bnj964  33019  bnj978  33025  bnj983  33027  bnj1039  33047  bnj1040  33048  bnj1123  33062  bnj1128  33066  bnj1398  33110  lfuhgr3  33177  cvmlift2lem1  33360  satfv0  33416  satf0  33430  satf0op  33435  satffunlem  33459  satffunlem1lem1  33460  satffunlem2lem1  33462  elmthm  33634  quad3  33724  3orit  33754  snres0  33771  ralxp3f  33781  dftr6  33813  eldm3  33823  elrn3  33824  elima4  33844  19.12b  33871  frpoins3xpg  33881  poxp2  33884  nosupbnd1lem4  33973  nosupbnd2lem1  33977  slenlt  34014  madeval2  34096  made0  34116  brtxp  34241  brtxp2  34242  brpprod  34246  brpprod3a  34247  elfix  34264  dffix2  34266  ellimits  34271  sscoid  34274  dffun10  34275  elfuns  34276  elsingles  34279  brimg  34298  brapply  34299  brsuccf  34302  funpartlem  34303  brrestrict  34310  dfrecs2  34311  dfrdg4  34312  brlb  34316  altopthc  34332  altopthd  34333  fvtransport  34393  hfext  34544  nn0prpw  34571  filnetlem4  34629  df3nandALT2  34648  bj-sbeq  35144  bj-csbsnlem  35146  bj-elsngl  35216  bj-eltag  35225  bj-tagex  35235  bj-projun  35242  bj-reabeq  35275  bj-disj2r  35276  bj-restuni  35326  bj-elid6  35399  bj-eldiag  35405  bj-eldiag2  35406  topdifinffinlem  35576  relowlpssretop  35593  fvineqsneq  35641  wl-3xorbi  35702  wl-2mintru1  35719  wl-df3maxtru1  35721  wl-dfclab  35805  phpreu  35819  poimirlem24  35859  poimirlem26  35861  poimirlem30  35865  areacirclem5  35927  isbnd2  35999  sbcalf  36330  sbcexf  36331  sbccom2  36341  sbccom2f  36342  sbccom2fi  36343  csbcom2fi  36344  anan  36442  br1cnvinxp  36476  idinxpssinxp2  36541  ineleq  36577  brabidgaw  36588  brabidga  36589  inxpxrn  36619  rnxrn  36622  cossssid2  36692  cossssid3  36693  cosscnvssid3  36700  dfeldisj3  36943  dfeldisj4  36944  antisymrelres  36987  dfmembpart2  36994  mpet3  37060  cpet2  37061  prtlem70  37081  prtlem16  37093  ishlat2  37577  pmapglb  37994  polval2N  38130  dicelval3  39404  mapdordlem1a  39858  isdomn5  40384  prjspeclsp  40659  fz1eqin  40799  7rexfrabdioph  40830  rmydioph  41045  dford4  41060  areaquad  41256  ifpan23  41293  ifpdfnan  41319  ifpdfxor  41320  ifpidg  41324  ifpid1g  41327  ifpim123g  41333  ifp1bi  41335  ifpimimb  41337  ifpororb  41338  ifpbibib  41343  rp-fakeuninass  41349  dfsucon  41356  minregex  41367  cllem0  41399  rababg  41407  elmapintrab  41410  elmapintab  41430  undmrnresiss  41438  dfxor4  41600  dfhe3  41609  dffrege115  41812  frege131  41828  frege133  41830  clsk1indlem4  41880  clsk1indlem1  41881  expandrexn  42135  rr-groth  42143  rr-grothshortbi  42147  undisjrab  42150  pm13.196a  42258  eelT11  42553  eelTT1  42556  eelT01  42557  eel0T1  42558  uunTT1  42639  uunTT1p1  42640  uunTT1p2  42641  uunT11  42642  uunT11p1  42643  uunT11p2  42644  uun111  42651  ssrabf  42890  rabssf  42895  disjinfi  42964  elicores  43313  fourierdlem42  43932  iundjiun  44241  2reu7  44860  2reu8  44861  2reu8i  44862  dfdfat2  44877  aovov0bi  44945  afv2orxorb  44977  afv2ndeffv0  45009  ichcircshi  45163  ichan  45164  icheq  45171  ichal  45175  prpair  45210  prproropf1olem0  45211  257prm  45270  fmtno4prmfac  45281  nnsum4primeseven  45509  nnsum4primesevenALTV  45510  uspgrsprf1  45566  opeliun2xp  45925  rrx2xpref1o  46321  isthincd2  46576  aacllem  46762