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

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  bibi1i  338  pm5.32  573  biadan  818  orbi1i  913  orass  921  or32  925  cases  1042  dn1  1057  3anidm  1103  an33rean  1485  nanbi  1500  excxor  1516  cadan  1609  cadcomb  1613  nic-axALT  1674  tbw-bijust  1698  rb-bijust  1749  nf2  1785  19.43  1882  19.43OLD  1883  3exdistr  1960  19.12vvv  1994  sbco4  2103  excom13  2165  sbcom2  2174  sbco4OLD  2176  sbn  2280  sbnf  2311  19.12vv  2345  eeeanv  2348  ee4anv  2349  ee4anvOLD  2350  2sb8ef  2354  sbel2x  2472  2sb8e  2528  dfmo  2589  sb8eulem  2591  2mo2  2640  2eu7  2651  2eu8  2652  sbabel  2924  3r19.43  3098  r19.23v  3156  2ralor  3203  rexcom13  3262  cbvreu  3384  rabrabi  3411  cgsex4g  3480  ceqsex2  3487  ceqsex2v  3488  ceqsex3v  3489  ceqsex4v  3490  ceqsex6v  3491  ceqsex8v  3492  ralrab2  3654  rexrab2  3656  reu2  3681  rmo4  3686  reu8  3689  rmo3f  3690  2reu5lem3  3713  sbcimdv  3807  reu8nf  3825  rmo2  3835  rmo3  3837  rmoanim  3842  ss2rab  4018  rabss  4019  ssrab  4020  dfdif3OLD  4065  symdifass  4209  dfss4  4216  undi  4232  indifdi  4241  undif3  4247  reuun2  4272  difin0ss  4320  disj  4397  disj4  4406  rabsssn  4618  disjsn  4661  snssb  4732  raldifsni  4744  ssunpr  4783  sspr  4784  sstp  4785  uni0b  4882  uni0c  4883  ssint  4911  intprg  4928  iunssf  4990  iunss  4991  iundif2  5019  disjor  5070  nfnid  5310  reusv2lem4  5336  ssextss  5391  exss  5400  eqvinop  5424  sbcop  5426  opcom  5438  opeqpr  5442  brtp  5460  brabsb  5468  opelopabf  5482  dfid3  5511  pofun  5539  opeliunxp  5680  opeliun2xp  5681  xpiundi  5684  brinxp2  5691  reliun  5753  exopxfr  5780  cnvuni  5823  dmopab3  5856  rnep  5863  dmxp  5865  rnopab3  5892  elres  5965  elsnres  5966  elrid  5991  cnvsym  6057  asymref2  6060  intirr  6061  cnvopab  6080  xpeq0  6103  difxp  6107  xpdifid  6111  ssrnres  6121  dminxp  6123  dfrel4v  6133  elid  6142  dmsnn0  6150  imaco  6194  rnco  6195  coeq0  6198  resssxp  6212  dfpo2  6238  snres0  6240  sspred  6252  frpoind  6284  sb8iota  6443  fun11  6550  isarep1  6565  dff1o4  6766  opabiota  6898  fvopab5  6956  eqfnfv3  6960  fvn0ssdmfun  7001  fnressn  7085  f13dfv  7202  dff1o6  7203  fliftel  7237  oprabidw  7371  oprabid  7372  eloprabga  7449  mpo2eqb  7472  ralrnmpo  7479  uniuni  7689  dflim3  7771  dfom2  7792  elxp4  7846  elxp5  7847  opabex3d  7891  opabex3rd  7892  opabex3  7893  el2xptp  7961  fsplit  8041  xporderlem  8051  ralxp3f  8061  frpoins3xpg  8064  poxp2  8067  suppvalbr  8088  dfrecs3  8286  tz7.48lem  8354  seqomlem2  8364  oaord  8456  oeeu  8512  nnaord  8528  ecid  8698  mptelixpg  8853  elixpsn  8855  xpsnen  8968  xpcomco  8974  xpassen  8978  omxpenlem  8985  modom  9129  brttrcl2  9598  ttrcltr  9600  rnttrcl  9606  frind  9634  tz9.12lem3  9673  rankxpsuc  9766  cp  9775  cardprclem  9863  infxpenlem  9895  dfac5lem1  10005  dfac5lem2  10006  dfac5lem5  10009  dfac10c  10021  kmlem3  10035  kmlem12  10044  kmlem13  10045  kmlem14  10046  kmlem15  10047  ackbij2  10124  cf0  10133  cflim2  10145  dffin7-2  10280  dfacfin7  10281  fin1a2lem12  10293  axdc3lem3  10334  cfpwsdom  10466  recmulnq  10846  genpass  10891  psslinpr  10913  suplem2pr  10935  opelreal  11012  ltxrlt  11174  addrid  11284  elnn0  12374  elxnn0  12447  elnn0z  12472  nnwos  12804  elxr  13006  xrnepnf  13008  elfzuzb  13409  4fvwrd4  13539  preduz  13541  elfzo2  13553  ssnn0fi  13880  sqeqori  14109  xpcogend  14868  cotr2g  14870  fsumcom2  15668  modfsummod  15688  fprodcom2  15878  rpnnen2lem12  16121  gcdcllem1  16397  isprm2  16580  isprm7  16606  pythagtriplem2  16716  infpn2  16812  4sqlem12  16855  initoid  17895  termoid  17896  eldmcoa  17959  oduposb  18220  gsumwspan  18707  smndex1basss  18766  smndex1mgm  18768  isnsg2  19022  isnsg4  19033  cycsubmel  19066  efgcpbllemb  19621  dmdprd  19866  dprdval  19871  dprdw  19878  dprd2d2  19912  dfrhm2  20346  brric2  20375  issubrg  20440  isdomn5  20579  islmim  20950  lbsextlem2  21050  cnfldfun  21259  cnfldfunOLD  21272  pzriprnglem3  21374  pjfval2  21600  opsrtoslem1  21944  ntreq0  22946  cmpcov2  23259  cmpsub  23269  2ndcdisj  23325  unisngl  23396  txbas  23436  elpt  23441  txkgen  23521  xkococn  23529  fbun  23709  trfil2  23756  fin1aufil  23801  alexsubALTlem3  23918  cnextcn  23936  qustgplem  23990  eltsms  24002  ustn0  24090  fmucndlem  24159  metrest  24393  restmetu  24439  isclmp  24978  srabn  25241  ellogdm  26529  1cubr  26733  leibpilem2  26832  dmarea  26848  vmasum  27108  dchrelbas2  27129  2lgslem4  27298  nosupbnd1lem4  27604  nosupbnd2lem1  27608  slenlt  27645  madeval2  27748  made0  27772  onsiso  28159  onsfi  28237  tgcgr4  28463  ltgov  28529  axlowdimlem13  28886  axeuclidlem  28894  numedglnl  29076  nbupgrres  29296  vtxd0nedgb  29421  rusgrprc  29523  usgr2pth0  29697  wspthsnwspthsnon  29848  isclwwlk  29915  clwwlkn1  29972  clwwlkn2  29975  clwwlknonel  30026  3pthdlem1  30095  iseupthf1o  30133  frgr3v  30206  fusgr2wsp2nb  30265  frgrregord013  30326  h2hcau  30910  h2hlm  30911  shlesb1i  31317  shne0i  31379  chnlei  31416  cmbr2i  31527  pjneli  31654  ho02i  31760  adjsym  31764  adjeu  31820  lnopeqi  31939  largei  32198  atoml2i  32314  cdj3lem3b  32371  or3di  32390  mo5f  32420  dmrab  32428  rabsspr  32433  rabsstp  32434  disjnf  32502  disjorf  32511  ssrelf  32550  ofpreima  32599  disjdsct  32636  1stpreima  32640  2ndpreima  32641  f1od2  32654  xrdifh  32715  nndiffz1  32721  ind1a  32795  prmidl0  33383  zarclsun  33851  ordtconnlem1  33905  measiuns  34198  elunirnmbfm  34233  eulerpartlemr  34355  eulerpartlemgh  34359  eulerpartlemn  34362  ballotlemodife  34479  bnj250  34681  bnj334  34693  bnj345  34694  bnj89  34701  bnj115  34705  bnj919  34747  bnj1304  34799  bnj92  34842  bnj124  34851  bnj126  34853  bnj154  34858  bnj155  34859  bnj523  34867  bnj526  34868  bnj540  34872  bnj581  34888  bnj916  34913  bnj929  34916  bnj964  34923  bnj978  34929  bnj983  34931  bnj1039  34951  bnj1040  34952  bnj1123  34966  bnj1128  34970  bnj1398  35014  lfuhgr3  35110  cvmlift2lem1  35292  satfv0  35348  satf0  35362  satf0op  35367  satffunlem  35391  satffunlem1lem1  35392  satffunlem2lem1  35394  elmthm  35566  quad3  35660  3orit  35706  dftr6  35741  eldm3  35751  elrn3  35752  elima4  35766  19.12b  35792  brtxp  35871  brtxp2  35872  brpprod  35876  brpprod3a  35877  elfix  35894  dffix2  35896  ellimits  35901  sscoid  35904  dffun10  35905  elfuns  35906  elsingles  35909  brimg  35928  brapply  35929  brsuccf  35932  funpartlem  35933  brrestrict  35940  dfrecs2  35941  dfrdg4  35942  brlb  35946  altopthc  35962  altopthd  35963  fvtransport  36023  hfext  36174  ss-ax8  36216  nn0prpw  36314  filnetlem4  36372  df3nandALT2  36391  bj-sbeq  36892  bj-csbsnlem  36894  bj-elsngl  36959  bj-eltag  36968  bj-tagex  36978  bj-projun  36985  bj-reabeq  37018  bj-disj2r  37019  bj-restuni  37088  bj-elid6  37161  bj-eldiag  37167  bj-eldiag2  37168  topdifinffinlem  37338  relowlpssretop  37355  fvineqsneq  37403  wl-3xorbi  37464  wl-2mintru1  37481  wl-df3maxtru1  37483  wl-dfclab  37587  phpreu  37601  poimirlem24  37641  poimirlem26  37643  poimirlem30  37647  areacirclem5  37709  isbnd2  37780  sbcalf  38111  sbcexf  38112  sbccom2  38122  sbccom2f  38123  sbccom2fi  38124  csbcom2fi  38125  anan  38220  br1cnvinxp  38248  idinxpssinxp2  38309  ineleq  38339  brabidgaw  38350  brabidga  38351  inxpxrn  38384  rnxrn  38387  cossssid2  38462  cossssid3  38463  cosscnvssid3  38470  dfeldisj3  38714  dfeldisj4  38715  antisymrelres  38758  dfmembpart2  38765  mpet3  38831  cpet2  38832  prtlem70  38853  prtlem16  38865  ishlat2  39349  pmapglb  39766  polval2N  39902  dicelval3  41176  mapdordlem1a  41630  redvmptabs  42350  fimgmcyclem  42523  fimgmcyc  42524  prjspeclsp  42602  sn-isghm  42663  abbibw  42667  fz1eqin  42759  7rexfrabdioph  42790  rmydioph  43004  dford4  43019  areaquad  43206  onsupmaxb  43229  onov0suclim  43264  nnoeomeqom  43302  tfsconcat0i  43335  faosnf0.11b  43417  ifpan23  43450  ifpdfnan  43476  ifpdfxor  43477  ifpidg  43481  ifpid1g  43484  ifpim123g  43490  ifp1bi  43492  ifpimimb  43494  ifpororb  43495  ifpbibib  43500  rp-fakeuninass  43506  dfsucon  43513  minregex  43524  cllem0  43556  rababg  43564  elmapintrab  43566  elmapintab  43586  undmrnresiss  43594  dfxor4  43756  dfhe3  43765  dffrege115  43968  frege131  43984  frege133  43986  clsk1indlem4  44034  clsk1indlem1  44035  expandrexn  44281  rr-groth  44289  rr-grothshortbi  44293  undisjrab  44296  pm13.196a  44404  eelT11  44696  eelTT1  44699  eelT01  44700  eel0T1  44701  uunTT1  44782  uunTT1p1  44783  uunTT1p2  44784  uunT11  44785  uunT11p1  44786  uunT11p2  44787  uun111  44794  xpwf  44954  permaxinf2lem  45002  permac8prim  45004  ssrabf  45108  rabssf  45113  disjinfi  45186  elicores  45530  fourierdlem42  46144  iundjiun  46455  2reu7  47109  2reu8  47110  2reu8i  47111  dfdfat2  47126  aovov0bi  47194  afv2orxorb  47226  afv2ndeffv0  47258  ichcircshi  47452  ichan  47453  icheq  47460  ichal  47464  prpair  47499  prproropf1olem0  47500  257prm  47559  fmtno4prmfac  47570  nnsum4primeseven  47798  nnsum4primesevenALTV  47799  clnbgrel  47826  isubgr3stgrlem4  47967  usgrexmpl2nb1  48030  usgrexmpl2nb2  48031  gpgprismgr4cycllem10  48102  uspgrsprf1  48145  rrx2xpref1o  48717  iinxp  48829  resinsn  48870  resinsnALT  48871  0funcALT  49087  catcsect  49397  isthincd2  49436  aacllem  49800