Theorem 3bitri 298

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

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  bibi1i  339  pm5.32  578  biadan  824  orbi1i  919  orass  927  or32  931  cases  1048  dn1  1063  3anidm  1109  an33rean  1491  nanbi  1507  excxor  1523  cadan  1616  cadcomb  1620  nic-axALT  1681  tbw-bijust  1705  rb-bijust  1756  nf2  1792  19.43  1889  19.43OLD  1890  3exdistr  1967  19.12vvv  2001  sbco4  2113  excom13  2175  sbcom2  2183  sbco4OLD  2185  sbn  2291  sbnf  2322  19.12vv  2355  eeeanv  2358  ee4anv  2359  ee4anvOLD  2360  2sb8ef  2364  sbel2x  2482  2sb8e  2538  dfmo2  2600  sb8eulem  2602  2mo2  2651  2eu7  2662  2eu8  2663  sbabel  2934  3r19.43  3109  r19.23v  3167  2ralor  3214  rexcom13  3273  cbvreu  3384  rabrabi  3411  cgsex4g  3479  ceqsex2  3484  ceqsex2v  3485  ceqsex3v  3486  ceqsex4v  3487  ceqsex6v  3488  ceqsex8v  3489  ralrab2  3646  rexrab2  3648  reu2  3673  rmo4  3678  reu8  3681  rmo3f  3682  2reu5lem3  3705  sbcimdv  3798  reu8nf  3816  rmo2  3826  rmo3  3828  rmoanim  3833  ss2rab  4007  rabss  4008  ssrab  4009  dfdif3OLD  4056  symdifass  4197  dfss4  4204  undi  4220  indifdi  4229  undif3  4235  reuun2  4260  difin0ss  4308  disj  4385  disj4  4394  rabsssn  4607  disjsn  4650  snssb  4721  raldifsni  4735  ssunpr  4772  sspr  4773  sstp  4774  uni0b  4871  uni0c  4872  ssint  4901  intprg  4918  iunssf  4979  iunssfOLD  4980  iunss  4981  iunssOLD  4982  iundif2  5010  disjor  5061  nfnid  5311  reusv2lem4  5337  ssextss  5399  exss  5409  eqvinop  5434  sbcop  5436  opcom  5449  opeqpr  5453  brtp  5472  brabsb  5480  opelopabf  5494  dfid3  5523  pofun  5551  opeliunxp  5692  opeliun2xp  5693  xpiundi  5696  brinxp2  5703  exopxfr  5792  cnvuni  5835  dmopab3  5868  rnep  5876  dmxp  5878  rnopab3  5905  elres  5979  elsnres  5980  elrid  6005  cnvsym  6071  asymref2  6074  intirr  6075  cnvopab  6094  xpeq0  6118  difxp  6122  xpdifid  6126  ssrnres  6136  dminxp  6138  dfrel4v  6148  elid  6157  dmsnn0  6165  imaco  6209  rnco  6210  rncoOLD  6211  coeq0  6214  resssxp  6228  dfpo2  6254  snres0  6256  sspred  6268  frpoind  6300  sb8iota  6459  fun11  6566  isarep1  6581  dff1o4  6782  opabiota  6916  fvopab5  6976  eqfnfv3  6980  fvn0ssdmfun  7022  fnressn  7108  f13dfv  7225  dff1o6  7226  fliftel  7260  oprabidw  7394  oprabid  7395  eloprabga  7472  mpo2eqb  7495  ralrnmpo  7502  uniuni  7712  dflim3  7794  dfom2  7815  elxp4  7869  elxp5  7870  opabex3d  7914  opabex3rd  7915  opabex3  7916  el2xptp  7984  fsplit  8063  xporderlem  8074  ralxp3f  8084  frpoins3xpg  8087  poxp2  8090  suppvalbr  8111  dfrecs3  8309  tz7.48lem  8377  seqomlem2  8387  oaord  8479  oeeu  8536  nnaord  8552  ecid  8724  mptelixpg  8880  elixpsn  8882  xpsnen  8996  xpcomco  9002  xpassen  9006  omxpenlem  9013  modom  9158  brttrcl2  9633  ttrcltr  9635  rnttrcl  9641  frind  9672  tz9.12lem3  9711  rankxpsuc  9804  cp  9813  cardprclem  9901  infxpenlem  9933  dfac5lem1  10043  dfac5lem2  10044  dfac5lem5  10047  dfac10c  10059  kmlem3  10073  kmlem12  10082  kmlem13  10083  kmlem14  10084  kmlem15  10085  ackbij2  10162  cf0  10171  cflim2  10183  dffin7-2  10318  dfacfin7  10319  fin1a2lem12  10331  axdc3lem3  10372  cfpwsdom  10505  recmulnq  10885  genpass  10930  psslinpr  10952  suplem2pr  10974  opelreal  11051  ltxrlt  11214  addrid  11324  ind1a  12168  elnn0  12437  elxnn0  12510  elnn0z  12535  nnwos  12863  elxr  13065  xrnepnf  13067  elfzuzb  13470  4fvwrd4  13600  preduz  13602  elfzo2  13614  ssnn0fi  13945  sqeqori  14174  xpcogend  14934  cotr2g  14936  fsumcom2  15734  modfsummod  15755  fprodcom2  15947  rpnnen2lem12  16190  gcdcllem1  16466  isprm2  16649  isprm7  16676  pythagtriplem2  16786  infpn2  16882  4sqlem12  16925  initoid  17966  termoid  17967  eldmcoa  18030  oduposb  18291  gsumwspan  18812  smndex1basss  18874  smndex1mgm  18876  isnsg2  19129  isnsg4  19140  cycsubmel  19173  efgcpbllemb  19728  dmdprd  19973  dprdval  19978  dprdw  19985  dprd2d2  20019  dfrhm2  20452  brric2  20485  issubrg  20550  isdomn5  20689  islmim  21059  lbsextlem2  21159  cnfldfun  21368  pzriprnglem3  21465  pjfval2  21691  opsrtoslem1  22038  ntreq0  23067  cmpcov2  23380  cmpsub  23390  2ndcdisj  23446  unisngl  23517  txbas  23557  elpt  23562  txkgen  23642  xkococn  23650  fbun  23830  trfil2  23877  fin1aufil  23922  alexsubALTlem3  24039  cnextcn  24057  qustgplem  24111  eltsms  24123  ustn0  24211  fmucndlem  24280  metrest  24514  restmetu  24560  isclmp  25089  srabn  25352  ellogdm  26628  1cubr  26831  leibpilem2  26930  dmarea  26946  vmasum  27204  dchrelbas2  27225  2lgslem4  27394  nosupbnd1lem4  27700  nosupbnd2lem1  27704  lenlts  27741  madeval2  27850  made0  27880  oniso  28288  onsfi  28373  tgcgr4  28624  ltgov  28690  axlowdimlem13  29048  axeuclidlem  29056  numedglnl  29238  nbupgrres  29458  vtxd0nedgb  29582  rusgrprc  29684  usgr2pth0  29858  wspthsnwspthsnon  30009  isclwwlk  30079  clwwlkn1  30136  clwwlkn2  30139  clwwlknonel  30190  3pthdlem1  30259  iseupthf1o  30297  frgr3v  30370  fusgr2wsp2nb  30429  frgrregord013  30490  h2hcau  31075  h2hlm  31076  shlesb1i  31482  shne0i  31544  chnlei  31581  cmbr2i  31692  pjneli  31819  ho02i  31925  adjsym  31929  adjeu  31985  lnopeqi  32104  largei  32363  atoml2i  32479  cdj3lem3b  32536  or3di  32553  mo5f  32583  dmrab  32591  rabsspr  32596  rabsstp  32597  disjnf  32666  disjorf  32675  ssrelf  32714  ofpreima  32764  disjdsct  32802  1stpreima  32806  2ndpreima  32807  f1od2  32818  xrdifh  32879  nndiffz1  32885  domnprodeq0  33364  prmidl0  33540  zarclsun  34061  ordtconnlem1  34115  measiuns  34408  elunirnmbfm  34443  eulerpartlemr  34565  eulerpartlemgh  34569  eulerpartlemn  34572  ballotlemodife  34689  bnj250  34891  bnj334  34903  bnj345  34904  bnj89  34911  bnj115  34915  bnj919  34957  bnj1304  35008  bnj92  35051  bnj124  35060  bnj126  35062  bnj154  35067  bnj155  35068  bnj523  35076  bnj526  35077  bnj540  35081  bnj581  35097  bnj916  35122  bnj929  35125  bnj964  35132  bnj978  35138  bnj983  35140  bnj1039  35160  bnj1040  35161  bnj1123  35175  bnj1128  35179  bnj1398  35223  lfuhgr3  35355  cvmlift2lem1  35537  satfv0  35593  satf0  35607  satf0op  35612  satffunlem  35636  satffunlem1lem1  35637  satffunlem2lem1  35639  elmthm  35811  quad3  35905  3orit  35951  dftr6  35986  eldm3  35996  elrn3  35997  elima4  36011  19.12b  36034  brtxp  36113  brtxp2  36114  brpprod  36118  brpprod3a  36119  elfix  36136  dffix2  36138  ellimits  36143  sscoid  36146  dffun10  36147  elfuns  36148  elsingles  36151  brimg  36170  brapply  36171  lemsuccf  36174  brsuccf  36175  funpartlem  36177  brrestrict  36184  dfrecs2  36185  dfrdg4  36186  brlb  36190  altopthc  36206  altopthd  36207  fvtransport  36267  hfext  36418  ss-ax8  36460  nn0prpw  36558  filnetlem4  36616  df3nandALT2  36635  regsfromregtco  36773  mh-prprimbi  36778  mh-regprimbi  36780  mh-infprim2bi  36782  mh-infprim3bi  36783  bj-sbeq  37261  bj-csbsnlem  37263  bj-elsngl  37328  bj-eltag  37337  bj-tagex  37347  bj-projun  37354  bj-reabeq  37387  bj-disj2r  37388  bj-axseprep  37434  bj-restuni  37462  bj-elid6  37537  bj-eldiag  37543  bj-eldiag2  37544  topdifinffinlem  37716  relowlpssretop  37733  fvineqsneq  37781  wl-3xorbi  37842  wl-2mintru1  37859  wl-df3maxtru1  37861  wl-dfclab  37963  phpreu  37978  poimirlem24  38018  poimirlem26  38020  poimirlem30  38024  areacirclem5  38086  isbnd2  38157  sbcalf  38488  sbcexf  38489  sbccom2  38499  sbccom2f  38500  sbccom2fi  38501  csbcom2fi  38502  anan  38609  br1cnvinxp  38633  idinxpssinxp2  38698  ineleq  38728  brabidgaw  38747  brabidga  38748  inxpxrn  38792  rnxrn  38795  dfsucmap3  38837  cossssid2  38932  cossssid3  38933  cosscnvssid3  38940  dfeldisj3  39185  dfeldisj4  39186  antisymrelres  39240  dfmembpart2  39247  mpet3  39324  cpet2  39325  prtlem70  39356  prtlem16  39368  ishlat2  39852  pmapglb  40269  polval2N  40405  dicelval3  41679  mapdordlem1a  42133  redvmptabs  42844  fimgmcyclem  43026  fimgmcyc  43027  prjspeclsp  43069  sn-isghm  43130  abbibw  43134  fz1eqin  43225  7rexfrabdioph  43252  rmydioph  43466  dford4  43481  areaquad  43668  onsupmaxb  43691  onov0suclim  43726  nnoeomeqom  43764  tfsconcat0i  43797  faosnf0.11b  43878  ifpan23  43911  ifpdfnan  43937  ifpdfxor  43938  ifpidg  43942  ifpid1g  43945  ifpim123g  43951  ifp1bi  43953  ifpimimb  43955  ifpororb  43956  ifpbibib  43961  rp-fakeuninass  43967  dfsucon  43974  minregex  43985  cllem0  44017  rababg  44025  elmapintrab  44027  elmapintab  44047  undmrnresiss  44055  dfxor4  44217  dfhe3  44226  dffrege115  44429  frege131  44445  frege133  44447  clsk1indlem4  44495  clsk1indlem1  44496  expandrexn  44742  rr-groth  44750  rr-grothshortbi  44754  undisjrab  44757  pm13.196a  44865  eelT11  45157  eelTT1  45160  eelT01  45161  eel0T1  45162  uunTT1  45243  uunTT1p1  45244  uunTT1p2  45245  uunT11  45246  uunT11p1  45247  uunT11p2  45248  uun111  45255  xpwf  45415  permaxinf2lem  45463  permac8prim  45465  ssrabf  45568  rabssf  45573  disjinfi  45646  elicores  45985  fourierdlem42  46599  iundjiun  46910  2reu7  47581  2reu8  47582  2reu8i  47583  dfdfat2  47598  aovov0bi  47666  afv2orxorb  47698  afv2ndeffv0  47730  ichcircshi  47936  ichan  47937  icheq  47944  ichal  47948  prpair  47983  prproropf1olem0  47984  257prm  48046  fmtno4prmfac  48057  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  clnbgrel  48326  isubgr3stgrlem4  48467  usgrexmpl2nb1  48530  usgrexmpl2nb2  48531  gpgprismgr4cycllem10  48602  uspgrsprf1  48645  rrx2xpref1o  49216  iinxp  49328  resinsn  49369  resinsnALT  49370  0funcALT  49585  catcsect  49895  isthincd2  49934  aacllem  50298