Theorem 3bitri 300

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  bibi1i  341  pm5.32  583  biadan  830  orbi1i  926  orass  934  or32  938  cases  1058  dn1  1073  3anidm  1121  an33rean  1514  nanbi  1530  excxor  1546  cadan  1639  cadcomb  1643  nic-axALT  1704  tbw-bijust  1728  rb-bijust  1779  nf2  1815  19.43  1912  19.43OLD  1913  3exdistr  1990  19.12vvv  2024  sbco4  2137  excom13  2199  sbcom2  2207  sbco4OLD  2209  sbn  2315  sbnf  2346  19.12vv  2379  eeeanv  2382  ee4anv  2383  ee4anvOLD  2384  2sb8ef  2388  sbel2x  2506  2sb8e  2562  dfmo2  2624  sb8eulem  2626  2mo2  2675  2eu7  2685  2eu8  2686  sbabel  2957  3r19.43  3134  r19.23v  3192  2ralor  3239  rexcom13  3298  cbvreu  3408  rabrabi  3435  cgsex4g  3501  ceqsex2  3505  ceqsex2v  3506  ceqsex3v  3507  ceqsex4v  3508  ceqsex6v  3509  ceqsex8v  3510  ralrab2  3662  rexrab2  3664  reu2  3689  rmo4  3694  reu8  3697  rmo3f  3698  2reu5lem3  3721  sbcimdv  3813  reu8nf  3831  rmo2  3841  rmo3  3843  rmoanim  3849  ss2rab  4024  rabss  4025  ssrab  4026  dfdif3OLD  4074  symdifass  4216  dfss4  4223  undi  4239  indifdi  4248  undif3  4254  reuun2  4279  difin0ss  4329  disj  4411  disj4  4420  rabsssn  4635  disjsn  4678  snssb  4749  raldifsni  4764  ssunpr  4800  sspr  4801  sstp  4802  uni0b  4900  uni0c  4901  ssint  4930  intprg  4947  iunssf  5008  iunssfOLD  5009  iunss  5010  iunssOLD  5011  iundif2  5039  disjor  5092  nfnid  5348  reusv2lem4  5374  ssextss  5436  exss  5446  eqvinop  5471  sbcop  5473  opcom  5486  opeqpr  5490  brtp  5509  brabsb  5517  opelopabf  5532  dfid3  5561  pofun  5589  opeliunxp  5730  opeliun2xp  5731  xpiundi  5734  brinxp2  5741  exopxfr  5831  cnvuni  5878  dmopab3  5911  rnep  5919  dmxp  5921  rnopab3  5948  elres  6021  elsnres  6022  elrid  6050  cnvsym  6116  asymref2  6119  intirr  6120  cnvopab  6139  xpeq0  6159  difxp  6163  xpdifid  6167  xpdifcnvepel  6168  ssrnres  6178  dminxp  6180  dfrel4v  6190  elid  6200  dmsnn0  6210  imaco  6254  rnco  6255  rncoOLD  6256  coeq0  6259  resssxp  6273  dfpo2  6299  snres0  6301  sspred  6313  frpoind  6345  sb8iota  6505  fun11  6612  isarep1  6626  dff1o4  6831  opabiota  6965  fvopab5  7025  eqfnfv3  7029  fvn0ssdmfun  7071  fnressn  7157  f13dfv  7274  dff1o6  7275  fliftel  7309  oprabidw  7443  oprabid  7444  eloprabga  7521  mpo2eqb  7544  ralrnmpo  7551  uniuni  7762  dflim3  7844  dfom2  7865  elxp4  7920  elxp5  7921  opabex3d  7963  opabex3rd  7964  opabex3  7965  el2xptp  8033  fsplit  8113  xporderlem  8124  ralxp3f  8134  frpoins3xpg  8137  poxp2  8140  suppvalbr  8161  dfrecs3  8360  tz7.48lem  8429  seqomlem2  8439  oaord  8533  oeeu  8590  nnaord  8606  ecid  8779  mptelixpg  8934  elixpsn  8936  xpsnen  9050  xpcomco  9056  xpassen  9060  omxpenlem  9067  modom  9212  brttrcl2  9684  ttrcltr  9686  rnttrcl  9692  frind  9723  tz9.12lem3  9762  rankxpsuc  9855  cp  9878  cardprclem  9966  infxpenlem  9998  dfac5lem1  10108  dfac5lem2  10109  dfac5lem5  10112  dfac10c  10123  kmlem3  10137  kmlem12  10146  kmlem13  10147  kmlem14  10148  kmlem15  10149  ackbij2  10226  cf0  10235  cflim2  10248  dffin7-2  10383  dfacfin7  10384  fin1a2lem12  10396  axdc3lem3  10437  cfpwsdom  10570  recmulnq  10950  genpass  10995  psslinpr  11017  suplem2pr  11039  opelreal  11116  ltxrlt  11281  addrid  11391  ind1a  12230  elnn0  12507  elxnn0  12580  elnn0z  12605  nnwos  12940  elxr  13142  xrnepnf  13144  elfzuzb  13547  4fvwrd4  13678  preduz  13680  elfzo2  13692  ssnn0fi  14023  sqeqori  14252  xpcogend  15013  cotr2g  15015  fsumcom2  15827  modfsummod  15848  fprodcom2  16040  rpnnen2lem12  16282  gcdcllem1  16558  isprm2  16741  isprm7  16768  pythagtriplem2  16878  infpn2  16974  4sqlem12  17017  initoid  18059  termoid  18060  eldmcoa  18123  oduposb  18384  gsumwspan  18906  smndex1basss  18968  smndex1mgm  18970  isnsg2  19223  isnsg4  19234  cycsubmel  19272  efgcpbllemb  19826  dmdprd  20071  dprdval  20076  dprdw  20083  dprd2d2  20117  dfrhm2  20557  brric2  20590  issubrg  20657  isdomn5  20796  islmim  21164  lbsextlem2  21264  prmidl0  21459  cnfldfun  21517  pzriprnglem3  21614  pjfval2  21840  opsrtoslem1  22187  ntreq0  23215  cmpcov2  23528  cmpsub  23538  2ndcdisj  23594  unisngl  23665  txbas  23705  elpt  23710  txkgen  23790  xkococn  23798  fbun  23978  trfil2  24025  fin1aufil  24070  alexsubALTlem3  24187  cnextcn  24205  qustgplem  24259  eltsms  24271  ustn0  24359  fmucndlem  24428  metrest  24662  restmetu  24708  isclmp  25237  srabn  25500  ellogdm  26785  1cubr  26988  leibpilem2  27087  dmarea  27103  vmasum  27361  dchrelbas2  27382  2lgslem4  27551  nosupbnd1lem4  27856  nosupbnd2lem1  27860  lenlts  27897  madeval2  28007  made0  28037  oniso  28445  onsfi  28530  tgcgr4  28781  ltgov  28847  plngrotlem2  29051  axlowdimlem13  29285  axeuclidlem  29293  numedglnl  29475  nbupgrres  29695  vtxd0nedgb  29819  rusgrprc  29921  usgr2pth0  30095  wspthsnwspthsnon  30246  isclwwlk  30316  clwwlkn1  30373  clwwlkn2  30376  clwwlknonel  30427  3pthdlem1  30496  iseupthf1o  30534  frgr3v  30607  fusgr2wsp2nb  30666  frgrregord013  30727  h2hcau  31312  h2hlm  31313  shlesb1i  31719  shne0i  31781  chnlei  31818  cmbr2i  31929  pjneli  32056  ho02i  32162  adjsym  32166  adjeu  32222  lnopeqi  32341  largei  32600  atoml2i  32716  cdj3lem3b  32773  or3di  32788  mo5f  32816  dmrab  32824  rabsspr  32828  rabsstp  32829  disjnf  32896  disjorf  32905  ssrelf  32941  ofpreima  32991  disjdsct  33029  1stpreima  33033  2ndpreima  33034  f1od2  33045  xrdifh  33106  nndiffz1  33112  domnprodeq0  33580  zarclsun  34241  ordtconnlem1  34295  measiuns  34588  elunirnmbfm  34623  eulerpartlemr  34745  eulerpartlemgh  34749  eulerpartlemn  34752  ballotlemodife  34869  bnj250  35071  bnj334  35083  bnj345  35084  bnj89  35091  bnj115  35095  bnj919  35137  bnj1304  35188  bnj92  35231  bnj124  35240  bnj126  35242  bnj154  35247  bnj155  35248  bnj523  35256  bnj526  35257  bnj540  35261  bnj581  35277  bnj916  35302  bnj929  35305  bnj964  35312  bnj978  35318  bnj983  35320  bnj1039  35340  bnj1040  35341  bnj1123  35355  bnj1128  35359  bnj1398  35403  lfuhgr3  35593  cvmlift2lem1  35775  satfv0  35831  satf0  35845  satf0op  35850  satffunlem  35874  satffunlem1lem1  35875  satffunlem2lem1  35877  elmthm  36049  quad3  36143  3orit  36189  dftr6  36224  eldm3  36234  elrn3  36235  elima4  36249  19.12b  36272  brtxp  36351  brtxp2  36352  brpprod  36356  brpprod3a  36357  elfix  36374  dffix2  36376  ellimits  36381  sscoid  36384  dffun10  36385  elfuns  36386  elsingles  36389  brimg  36408  brapply  36409  lemsuccf  36412  brsuccf  36413  funpartlem  36415  brrestrict  36422  dfrecs2  36423  dfrdg4  36424  brlb  36428  altopthc  36444  altopthd  36445  fvtransport  36505  hfext  36656  ss-ax8  36718  nn0prpw  36815  filnetlem4  36873  df3nandALT2  36892  regsfromregtco  37030  mh-prprimbi  37035  mh-regprimbi  37037  mh-infprim2bi  37039  mh-infprim3bi  37040  bj-sbeq  37517  bj-csbsnlem  37519  bj-elsngl  37585  bj-eltag  37594  bj-tagex  37604  bj-projun  37611  bj-reabeq  37644  bj-disj2r  37645  bj-axseprep  37692  bj-restuni  37720  bj-elid6  37795  bj-eldiag  37801  bj-eldiag2  37802  topdifinffinlem  37974  relowlpssretop  37991  fvineqsneq  38039  wl-3xorbi  38100  wl-2mintru1  38117  wl-df3maxtru1  38119  wl-dfclab  38221  phpreu  38236  poimirlem24  38276  poimirlem26  38278  poimirlem30  38282  areacirclem5  38344  isbnd2  38415  sbcalf  38744  sbcexf  38745  sbccom2  38755  sbccom2f  38756  sbccom2fi  38757  csbcom2fi  38758  anan  38865  br1cnvinxp  38889  idinxpssinxp2  38954  ineleq  38984  brabidgaw  39003  brabidga  39004  inxpxrn  39048  rnxrn  39051  dfsucmap3  39093  cossssid2  39188  cossssid3  39189  cosscnvssid3  39196  dfeldisj3  39441  dfeldisj4  39442  antisymrelres  39496  dfmembpart2  39503  mpet3  39580  cpet2  39581  prtlem70  39612  prtlem16  39624  ishlat2  40108  pmapglb  40525  polval2N  40661  dicelval3  41935  mapdordlem1a  42389  redvmptabs  43102  fimgmcyclem  43284  fimgmcyc  43285  prjspeclsp  43327  sn-isghm  43388  abbibw  43392  fz1eqin  43483  7rexfrabdioph  43510  rmydioph  43724  dford4  43739  areaquad  43926  onsupmaxb  43949  onov0suclim  43984  nnoeomeqom  44022  tfsconcat0i  44055  faosnf0.11b  44136  ifpan23  44169  ifpdfnan  44195  ifpdfxor  44196  ifpidg  44200  ifpid1g  44203  ifpim123g  44209  ifp1bi  44211  ifpimimb  44213  ifpororb  44214  ifpbibib  44219  rp-fakeuninass  44225  dfsucon  44232  minregex  44243  cllem0  44275  rababg  44283  elmapintrab  44285  elmapintab  44305  undmrnresiss  44313  dfxor4  44475  dfhe3  44484  dffrege115  44687  frege131  44703  frege133  44705  clsk1indlem4  44753  clsk1indlem1  44754  expandrexn  44984  rr-groth  44992  rr-grothshortbi  44996  undisjrab  44999  pm13.196a  45107  eelT11  45398  eelTT1  45401  eelT01  45402  eel0T1  45403  uunTT1  45484  uunTT1p1  45485  uunTT1p2  45486  uunT11  45487  uunT11p1  45488  uunT11p2  45489  uun111  45496  xpwf  45656  permaxinf2lem  45704  permac8prim  45706  ssrabf  45815  rabssf  45820  disjinfi  45893  elicores  46232  fourierdlem42  46846  iundjiun  47157  2reu7  47831  2reu8  47832  2reu8i  47833  dfdfat2  47848  aovov0bi  47916  afv2orxorb  47948  afv2ndeffv0  47980  ichcircshi  48186  ichan  48187  icheq  48194  ichal  48198  prpair  48233  prproropf1olem0  48234  257prm  48296  fmtno4prmfac  48307  nnsum4primeseven  48548  nnsum4primesevenALTV  48549  clnbgrel  48576  isubgr3stgrlem4  48717  usgrexmpl2nb1  48780  usgrexmpl2nb2  48781  gpgprismgr4cycllem10  48852  uspgrsprf1  48895  rrx2xpref1o  49481  iinxp  49592  resinsn  49633  resinsnALT  49634  0funcALT  49849  catcsect  50159  isthincd2  50198  alsanmo  50571  ralsanmo  50572  aacllem  50584