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  1501  excxor  1517  cadan  1610  cadcomb  1614  nic-axALT  1675  tbw-bijust  1699  rb-bijust  1750  nf2  1786  19.43  1883  19.43OLD  1884  3exdistr  1961  19.12vvv  1995  sbco4  2107  excom13  2169  sbcom2  2178  sbco4OLD  2180  sbn  2284  sbnf  2315  19.12vv  2349  eeeanv  2352  ee4anv  2353  ee4anvOLD  2354  2sb8ef  2358  sbel2x  2476  2sb8e  2532  dfmo  2593  sb8eulem  2595  2mo2  2644  2eu7  2655  2eu8  2656  sbabel  2928  3r19.43  3102  r19.23v  3160  2ralor  3207  rexcom13  3266  cbvreu  3388  rabrabi  3415  cgsex4g  3484  ceqsex2  3490  ceqsex2v  3491  ceqsex3v  3492  ceqsex4v  3493  ceqsex6v  3494  ceqsex8v  3495  ralrab2  3653  rexrab2  3655  reu2  3680  rmo4  3685  reu8  3688  rmo3f  3689  2reu5lem3  3712  sbcimdv  3806  reu8nf  3824  rmo2  3834  rmo3  3836  rmoanim  3841  ss2rab  4018  rabss  4019  ssrab  4020  dfdif3OLD  4067  symdifass  4211  dfss4  4218  undi  4234  indifdi  4243  undif3  4249  reuun2  4274  difin0ss  4322  disj  4399  disj4  4408  rabsssn  4620  disjsn  4663  snssb  4734  raldifsni  4746  ssunpr  4785  sspr  4786  sstp  4787  uni0b  4884  uni0c  4885  ssint  4914  intprg  4931  iunssf  4993  iunssfOLD  4994  iunss  4995  iunssOLD  4996  iundif2  5024  disjor  5075  nfnid  5315  reusv2lem4  5341  ssextss  5396  exss  5406  eqvinop  5430  sbcop  5432  opcom  5444  opeqpr  5448  brtp  5466  brabsb  5474  opelopabf  5488  dfid3  5517  pofun  5545  opeliunxp  5686  opeliun2xp  5687  xpiundi  5690  brinxp2  5697  exopxfr  5787  cnvuni  5830  dmopab3  5863  rnep  5871  dmxp  5873  rnopab3  5900  elres  5973  elsnres  5974  elrid  5999  cnvsym  6065  asymref2  6068  intirr  6069  cnvopab  6088  xpeq0  6112  difxp  6116  xpdifid  6120  ssrnres  6130  dminxp  6132  dfrel4v  6142  elid  6151  dmsnn0  6159  imaco  6203  rnco  6204  rncoOLD  6205  coeq0  6208  resssxp  6222  dfpo2  6248  snres0  6250  sspred  6262  frpoind  6294  sb8iota  6453  fun11  6560  isarep1  6575  dff1o4  6776  opabiota  6910  fvopab5  6968  eqfnfv3  6972  fvn0ssdmfun  7013  fnressn  7097  f13dfv  7214  dff1o6  7215  fliftel  7249  oprabidw  7383  oprabid  7384  eloprabga  7461  mpo2eqb  7484  ralrnmpo  7491  uniuni  7701  dflim3  7783  dfom2  7804  elxp4  7858  elxp5  7859  opabex3d  7903  opabex3rd  7904  opabex3  7905  el2xptp  7973  fsplit  8053  xporderlem  8063  ralxp3f  8073  frpoins3xpg  8076  poxp2  8079  suppvalbr  8100  dfrecs3  8298  tz7.48lem  8366  seqomlem2  8376  oaord  8468  oeeu  8524  nnaord  8540  ecid  8710  mptelixpg  8865  elixpsn  8867  xpsnen  8981  xpcomco  8987  xpassen  8991  omxpenlem  8998  modom  9142  brttrcl2  9611  ttrcltr  9613  rnttrcl  9619  frind  9650  tz9.12lem3  9689  rankxpsuc  9782  cp  9791  cardprclem  9879  infxpenlem  9911  dfac5lem1  10021  dfac5lem2  10022  dfac5lem5  10025  dfac10c  10037  kmlem3  10051  kmlem12  10060  kmlem13  10061  kmlem14  10062  kmlem15  10063  ackbij2  10140  cf0  10149  cflim2  10161  dffin7-2  10296  dfacfin7  10297  fin1a2lem12  10309  axdc3lem3  10350  cfpwsdom  10482  recmulnq  10862  genpass  10907  psslinpr  10929  suplem2pr  10951  opelreal  11028  ltxrlt  11190  addrid  11300  elnn0  12390  elxnn0  12463  elnn0z  12488  nnwos  12815  elxr  13017  xrnepnf  13019  elfzuzb  13420  4fvwrd4  13550  preduz  13552  elfzo2  13564  ssnn0fi  13894  sqeqori  14123  xpcogend  14883  cotr2g  14885  fsumcom2  15683  modfsummod  15703  fprodcom2  15893  rpnnen2lem12  16136  gcdcllem1  16412  isprm2  16595  isprm7  16621  pythagtriplem2  16731  infpn2  16827  4sqlem12  16870  initoid  17910  termoid  17911  eldmcoa  17974  oduposb  18235  gsumwspan  18756  smndex1basss  18815  smndex1mgm  18817  isnsg2  19070  isnsg4  19081  cycsubmel  19114  efgcpbllemb  19669  dmdprd  19914  dprdval  19919  dprdw  19926  dprd2d2  19960  dfrhm2  20394  brric2  20423  issubrg  20488  isdomn5  20627  islmim  20998  lbsextlem2  21098  cnfldfun  21307  cnfldfunOLD  21320  pzriprnglem3  21422  pjfval2  21648  opsrtoslem1  21991  ntreq0  22993  cmpcov2  23306  cmpsub  23316  2ndcdisj  23372  unisngl  23443  txbas  23483  elpt  23488  txkgen  23568  xkococn  23576  fbun  23756  trfil2  23803  fin1aufil  23848  alexsubALTlem3  23965  cnextcn  23983  qustgplem  24037  eltsms  24049  ustn0  24137  fmucndlem  24206  metrest  24440  restmetu  24486  isclmp  25025  srabn  25288  ellogdm  26576  1cubr  26780  leibpilem2  26879  dmarea  26895  vmasum  27155  dchrelbas2  27176  2lgslem4  27345  nosupbnd1lem4  27651  nosupbnd2lem1  27655  slenlt  27692  madeval2  27795  made0  27819  onsiso  28206  onsfi  28284  tgcgr4  28510  ltgov  28576  axlowdimlem13  28934  axeuclidlem  28942  numedglnl  29124  nbupgrres  29344  vtxd0nedgb  29469  rusgrprc  29571  usgr2pth0  29745  wspthsnwspthsnon  29896  isclwwlk  29966  clwwlkn1  30023  clwwlkn2  30026  clwwlknonel  30077  3pthdlem1  30146  iseupthf1o  30184  frgr3v  30257  fusgr2wsp2nb  30316  frgrregord013  30377  h2hcau  30961  h2hlm  30962  shlesb1i  31368  shne0i  31430  chnlei  31467  cmbr2i  31578  pjneli  31705  ho02i  31811  adjsym  31815  adjeu  31871  lnopeqi  31990  largei  32249  atoml2i  32365  cdj3lem3b  32422  or3di  32440  mo5f  32470  dmrab  32478  rabsspr  32483  rabsstp  32484  disjnf  32552  disjorf  32561  ssrelf  32600  ofpreima  32649  disjdsct  32688  1stpreima  32692  2ndpreima  32693  f1od2  32706  xrdifh  32767  nndiffz1  32773  ind1a  32845  prmidl0  33422  zarclsun  33904  ordtconnlem1  33958  measiuns  34251  elunirnmbfm  34286  eulerpartlemr  34408  eulerpartlemgh  34412  eulerpartlemn  34415  ballotlemodife  34532  bnj250  34734  bnj334  34746  bnj345  34747  bnj89  34754  bnj115  34758  bnj919  34800  bnj1304  34852  bnj92  34895  bnj124  34904  bnj126  34906  bnj154  34911  bnj155  34912  bnj523  34920  bnj526  34921  bnj540  34925  bnj581  34941  bnj916  34966  bnj929  34969  bnj964  34976  bnj978  34982  bnj983  34984  bnj1039  35004  bnj1040  35005  bnj1123  35019  bnj1128  35023  bnj1398  35067  lfuhgr3  35185  cvmlift2lem1  35367  satfv0  35423  satf0  35437  satf0op  35442  satffunlem  35466  satffunlem1lem1  35467  satffunlem2lem1  35469  elmthm  35641  quad3  35735  3orit  35781  dftr6  35816  eldm3  35826  elrn3  35827  elima4  35841  19.12b  35864  brtxp  35943  brtxp2  35944  brpprod  35948  brpprod3a  35949  elfix  35966  dffix2  35968  ellimits  35973  sscoid  35976  dffun10  35977  elfuns  35978  elsingles  35981  brimg  36000  brapply  36001  lemsuccf  36004  brsuccf  36005  funpartlem  36007  brrestrict  36014  dfrecs2  36015  dfrdg4  36016  brlb  36020  altopthc  36036  altopthd  36037  fvtransport  36097  hfext  36248  ss-ax8  36290  nn0prpw  36388  filnetlem4  36446  df3nandALT2  36465  bj-sbeq  36966  bj-csbsnlem  36968  bj-elsngl  37033  bj-eltag  37042  bj-tagex  37052  bj-projun  37059  bj-reabeq  37092  bj-disj2r  37093  bj-restuni  37162  bj-elid6  37235  bj-eldiag  37241  bj-eldiag2  37242  topdifinffinlem  37412  relowlpssretop  37429  fvineqsneq  37477  wl-3xorbi  37538  wl-2mintru1  37555  wl-df3maxtru1  37557  wl-dfclab  37650  phpreu  37665  poimirlem24  37705  poimirlem26  37707  poimirlem30  37711  areacirclem5  37773  isbnd2  37844  sbcalf  38175  sbcexf  38176  sbccom2  38186  sbccom2f  38187  sbccom2fi  38188  csbcom2fi  38189  anan  38291  br1cnvinxp  38314  idinxpssinxp2  38377  ineleq  38407  brabidgaw  38418  brabidga  38419  inxpxrn  38463  rnxrn  38466  dfsucmap3  38497  cossssid2  38591  cossssid3  38592  cosscnvssid3  38599  dfeldisj3  38838  dfeldisj4  38839  antisymrelres  38882  dfmembpart2  38889  mpet3  38955  cpet2  38956  prtlem70  38977  prtlem16  38989  ishlat2  39473  pmapglb  39890  polval2N  40026  dicelval3  41300  mapdordlem1a  41754  redvmptabs  42479  fimgmcyclem  42652  fimgmcyc  42653  prjspeclsp  42731  sn-isghm  42792  abbibw  42796  fz1eqin  42887  7rexfrabdioph  42918  rmydioph  43132  dford4  43147  areaquad  43334  onsupmaxb  43357  onov0suclim  43392  nnoeomeqom  43430  tfsconcat0i  43463  faosnf0.11b  43545  ifpan23  43578  ifpdfnan  43604  ifpdfxor  43605  ifpidg  43609  ifpid1g  43612  ifpim123g  43618  ifp1bi  43620  ifpimimb  43622  ifpororb  43623  ifpbibib  43628  rp-fakeuninass  43634  dfsucon  43641  minregex  43652  cllem0  43684  rababg  43692  elmapintrab  43694  elmapintab  43714  undmrnresiss  43722  dfxor4  43884  dfhe3  43893  dffrege115  44096  frege131  44112  frege133  44114  clsk1indlem4  44162  clsk1indlem1  44163  expandrexn  44409  rr-groth  44417  rr-grothshortbi  44421  undisjrab  44424  pm13.196a  44532  eelT11  44824  eelTT1  44827  eelT01  44828  eel0T1  44829  uunTT1  44910  uunTT1p1  44911  uunTT1p2  44912  uunT11  44913  uunT11p1  44914  uunT11p2  44915  uun111  44922  xpwf  45082  permaxinf2lem  45130  permac8prim  45132  ssrabf  45236  rabssf  45241  disjinfi  45314  elicores  45658  fourierdlem42  46272  iundjiun  46583  2reu7  47236  2reu8  47237  2reu8i  47238  dfdfat2  47253  aovov0bi  47321  afv2orxorb  47353  afv2ndeffv0  47385  ichcircshi  47579  ichan  47580  icheq  47587  ichal  47591  prpair  47626  prproropf1olem0  47627  257prm  47686  fmtno4prmfac  47697  nnsum4primeseven  47925  nnsum4primesevenALTV  47926  clnbgrel  47953  isubgr3stgrlem4  48094  usgrexmpl2nb1  48157  usgrexmpl2nb2  48158  gpgprismgr4cycllem10  48229  uspgrsprf1  48272  rrx2xpref1o  48844  iinxp  48956  resinsn  48997  resinsnALT  48998  0funcALT  49214  catcsect  49524  isthincd2  49563  aacllem  49927