Theorem 3bitri 297

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  339  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  norassOLD  1536  cadan  1611  cadcomb  1615  nic-axALT  1677  tbw-bijust  1701  rb-bijust  1752  nf2  1788  19.43  1886  19.43OLD  1887  3exdistr  1965  19.12vvv  1993  sbcom2  2162  excom13  2165  sbco4  2276  sbn  2278  19.12vv  2346  eeeanv  2349  ee4anv  2350  2sb8ef  2355  sbel2x  2475  2sb8e  2536  dfmo  2597  sb8eulem  2599  2mo2  2650  2eu7  2660  2eu8  2661  sbabel  2942  r19.26-3  3098  r19.23v  3209  rexcomOLD  3286  ralcom13  3287  rexcom13  3288  2ralor  3297  cbvreuwOLD  3378  cbvreu  3382  ceqsralt  3464  ceqsalv  3468  ceqsex2  3483  ceqsex2v  3484  ceqsex4v  3486  ralrab2  3636  rexrab2  3638  reu2  3661  rmo4  3666  reu8  3669  rmo3f  3670  2reu5lem3  3693  sbc3an  3787  sbcimdv  3791  reu8nf  3811  rmo2  3821  rmo3  3823  rmoanim  3828  dfss2OLD  3909  ss2rab  4005  rabss  4006  ssrab  4007  dfdif3  4050  symdifass  4186  dfss4  4193  undi  4209  indifdi  4218  undif3  4225  difin2  4226  difin0ss  4303  ab0OLD  4310  disj  4382  disjOLD  4383  disj4  4393  rabsssn  4604  disjsn  4648  raldifsni  4729  ssunpr  4766  sspr  4767  sstp  4768  uni0b  4868  uni0c  4869  ssint  4896  intprg  4913  iunssf  4975  iunss  4976  iundif2  5004  disjor  5055  nfnid  5299  reusv2lem4  5325  ssextss  5370  exss  5379  eqvinop  5402  sbcop  5404  opcom  5416  opeqpr  5420  brabsb  5445  opelopabf  5459  dfid3  5493  pofun  5522  opeliunxp  5655  xpiundi  5658  brinxp2  5665  reliun  5728  exopxfr  5755  cnvuni  5798  dmopab3  5831  rnep  5839  elres  5933  elsnres  5934  elrid  5956  asymref2  6027  intirr  6028  xpeq0  6068  xpdifid  6076  ssrnres  6086  dminxp  6088  dfrel4v  6098  elid  6107  dmsnn0  6115  rnco  6160  coeq0  6163  resssxp  6177  dfpo2  6203  sspred  6215  frpoind  6249  wfiOLD  6258  sb8iota  6407  dffun2OLD  6448  fun11  6515  isarep1  6530  isarep1OLD  6531  dff1o4  6733  opabiota  6860  fvopab5  6916  eqfnfv3  6920  fvn0ssdmfun  6961  fnressn  7039  f13dfv  7155  dff1o6  7156  fliftel  7189  oprabidw  7315  oprabid  7316  eloprabga  7391  mpo2eqb  7415  ralrnmpo  7421  uniuni  7621  dflim3  7703  dfom2  7723  elxp4  7778  elxp5  7779  opabex3d  7817  opabex3rd  7818  opabex3  7819  el2xptp  7886  fsplit  7966  xporderlem  7977  dfrecs3  8212  dfrecs3OLD  8213  tz7.48lem  8281  seqomlem2  8291  oaord  8387  oeeu  8443  nnaord  8459  ecid  8580  mptelixpg  8732  elixpsn  8734  xpsnen  8851  xpcomco  8858  xpassen  8862  omxpenlem  8869  dom0OLD  8899  modom  9032  brttrcl2  9481  ttrcltr  9483  rnttrcl  9489  frind  9517  tz9.12lem3  9556  rankxpsuc  9649  cp  9658  cardprclem  9746  infxpenlem  9778  dfac5lem1  9888  dfac5lem2  9889  dfac5lem5  9892  dfac10c  9903  kmlem3  9917  kmlem12  9926  kmlem13  9927  kmlem14  9928  kmlem15  9929  ackbij2  10008  cf0  10016  cflim2  10028  dffin7-2  10163  dfacfin7  10164  fin1a2lem12  10176  axdc3lem3  10217  cfpwsdom  10349  recmulnq  10729  genpass  10774  psslinpr  10796  suplem2pr  10818  opelreal  10895  ltxrlt  11054  addid1  11164  elnn0  12244  elxnn0  12316  elnn0z  12341  nnwos  12664  elxr  12861  xrnepnf  12863  elfzuzb  13259  4fvwrd4  13385  preduz  13387  elfzo2  13399  ssnn0fi  13714  sqeqori  13939  xpcogend  14694  cotr2g  14696  fsumcom2  15495  modfsummod  15515  fprodcom2  15703  rpnnen2lem12  15943  gcdcllem1  16215  isprm2  16396  isprm7  16422  pythagtriplem2  16527  infpn2  16623  4sqlem12  16666  initoid  17725  termoid  17726  eldmcoa  17789  oduposb  18056  gsumwspan  18494  smndex1basss  18553  smndex1mgm  18555  isnsg2  18793  isnsg4  18804  cycsubmel  18828  efgcpbllemb  19370  dmdprd  19610  dprdval  19615  dprdw  19622  dprd2d2  19656  dfrhm2  19970  brric2  19998  issubrg  20033  islmim  20333  lbsextlem2  20430  cnfldfun  20618  pjfval2  20925  opsrtoslem1  21271  ntreq0  22237  cmpcov2  22550  cmpsub  22560  2ndcdisj  22616  unisngl  22687  txbas  22727  elpt  22732  txkgen  22812  xkococn  22820  fbun  23000  trfil2  23047  fin1aufil  23092  alexsubALTlem3  23209  cnextcn  23227  qustgplem  23281  eltsms  23293  ustn0  23381  fmucndlem  23452  metrest  23689  restmetu  23735  isclmp  24269  srabn  24533  ellogdm  25803  1cubr  26001  leibpilem2  26100  dmarea  26116  vmasum  26373  dchrelbas2  26394  2lgslem4  26563  tgcgr4  26901  ltgov  26967  axlowdimlem13  27331  axeuclidlem  27339  numedglnl  27523  nbupgrres  27740  vtxd0nedgb  27864  rusgrprc  27966  usgr2pth0  28142  wspthsnwspthsnon  28290  isclwwlk  28357  clwwlkn1  28414  clwwlkn2  28417  clwwlknonel  28468  3pthdlem1  28537  iseupthf1o  28575  frgr3v  28648  fusgr2wsp2nb  28707  frgrregord013  28768  h2hcau  29350  h2hlm  29351  shlesb1i  29757  shne0i  29819  chnlei  29856  cmbr2i  29967  pjneli  30094  ho02i  30200  adjsym  30204  adjeu  30260  lnopeqi  30379  largei  30638  atoml2i  30754  cdj3lem3b  30811  or3di  30819  mo5f  30846  dmrab  30853  disjnf  30918  disjorf  30927  ssrelf  30964  ofpreima  31011  disjdsct  31044  1stpreima  31048  2ndpreima  31049  f1od2  31065  xrdifh  31110  nndiffz1  31116  prmidl0  31635  zarclsun  31829  ordtconnlem1  31883  ind1a  31996  measiuns  32194  elunirnmbfm  32229  eulerpartlemr  32350  eulerpartlemgh  32354  eulerpartlemn  32357  ballotlemodife  32473  bnj250  32689  bnj334  32701  bnj345  32702  bnj89  32709  bnj115  32713  bnj919  32756  bnj1304  32808  bnj92  32851  bnj124  32860  bnj126  32862  bnj154  32867  bnj155  32868  bnj523  32876  bnj526  32877  bnj540  32881  bnj581  32897  bnj916  32922  bnj929  32925  bnj964  32932  bnj978  32938  bnj983  32940  bnj1039  32960  bnj1040  32961  bnj1123  32975  bnj1128  32979  bnj1398  33023  lfuhgr3  33090  cvmlift2lem1  33273  satfv0  33329  satf0  33343  satf0op  33348  satffunlem  33372  satffunlem1lem1  33373  satffunlem2lem1  33375  elmthm  33547  quad3  33637  3orit  33667  snres0  33684  ralxp3f  33694  brtp  33726  dftr6  33727  eldm3  33737  elrn3  33738  elima4  33759  19.12b  33786  frpoins3xpg  33796  poxp2  33799  nosupbnd1lem4  33923  nosupbnd2lem1  33927  slenlt  33964  madeval2  34046  made0  34066  brtxp  34191  brtxp2  34192  brpprod  34196  brpprod3a  34197  elfix  34214  dffix2  34216  ellimits  34221  sscoid  34224  dffun10  34225  elfuns  34226  elsingles  34229  brimg  34248  brapply  34249  brsuccf  34252  funpartlem  34253  brrestrict  34260  dfrecs2  34261  dfrdg4  34262  brlb  34266  altopthc  34282  altopthd  34283  fvtransport  34343  hfext  34494  nn0prpw  34521  filnetlem4  34579  df3nandALT2  34598  bj-sbeq  35095  bj-csbsnlem  35097  bj-elsngl  35167  bj-eltag  35176  bj-tagex  35186  bj-projun  35193  bj-reabeq  35226  bj-disj2r  35227  bj-restuni  35277  bj-elid6  35350  bj-eldiag  35356  bj-eldiag2  35357  topdifinffinlem  35527  relowlpssretop  35544  fvineqsneq  35592  wl-3xorbi  35653  wl-2mintru1  35670  wl-df3maxtru1  35672  wl-dfclab  35756  phpreu  35770  poimirlem24  35810  poimirlem26  35812  poimirlem30  35816  areacirclem5  35878  isbnd2  35950  sbcalf  36281  sbcexf  36282  sbccom2  36292  sbccom2f  36293  sbccom2fi  36294  csbcom2fi  36295  anan  36388  idinxpssinxp2  36460  ineleq  36493  brabidgaw  36502  brabidga  36503  inxpxrn  36528  rnxrn  36531  cossssid2  36593  cossssid3  36594  cosscnvssid3  36601  dfeldisj3  36837  dfeldisj4  36838  prtlem70  36878  prtlem16  36890  ishlat2  37374  pmapglb  37791  polval2N  37927  dicelval3  39201  mapdordlem1a  39655  isdomn5  40178  prjspeclsp  40458  fz1eqin  40598  7rexfrabdioph  40629  rmydioph  40843  dford4  40858  areaquad  41054  ifpan23  41074  ifpdfnan  41100  ifpdfxor  41101  ifpidg  41105  ifpid1g  41108  ifpim123g  41114  ifp1bi  41116  ifpimimb  41118  ifpororb  41119  ifpbibib  41124  rp-fakeuninass  41130  dfsucon  41137  minregex  41148  cllem0  41180  rababg  41188  elmapintrab  41191  elmapintab  41211  undmrnresiss  41219  ss2iundf  41274  dfxor4  41381  dfhe3  41390  dffrege115  41593  frege131  41609  frege133  41611  clsk1indlem4  41661  clsk1indlem1  41662  expandrexn  41916  rr-groth  41924  rr-grothshortbi  41928  undisjrab  41931  pm13.196a  42039  eelT11  42334  eelTT1  42337  eelT01  42338  eel0T1  42339  uunTT1  42420  uunTT1p1  42421  uunTT1p2  42422  uunT11  42423  uunT11p1  42424  uunT11p2  42425  uun111  42432  ssrabf  42671  rabssf  42675  disjinfi  42738  elicores  43078  fourierdlem42  43697  iundjiun  44005  2reu7  44614  2reu8  44615  2reu8i  44616  dfdfat2  44631  aovov0bi  44699  afv2orxorb  44731  afv2ndeffv0  44763  ichcircshi  44917  ichan  44918  icheq  44925  ichal  44929  prpair  44964  prproropf1olem0  44965  257prm  45024  fmtno4prmfac  45035  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  uspgrsprf1  45320  opeliun2xp  45679  rrx2xpref1o  46075  isthincd2  46330  aacllem  46516