Theorem 3bitri 296

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  338  pm5.32  573  biadan  815  orbi1i  910  orass  918  or32  922  cases  1039  dn1  1054  3anidm  1102  an3andi  1480  an33rean  1481  an33reanOLD  1482  nanbi  1492  excxor  1509  norassOLD  1536  cadan  1612  cadcomb  1616  nic-axALT  1678  tbw-bijust  1702  rb-bijust  1753  nf2  1789  19.43  1886  19.43OLD  1887  3exdistr  1965  19.12vvv  1993  sbcom2  2163  excom13  2166  sbco4  2278  sbn  2280  19.12vv  2347  eeeanv  2350  ee4anv  2351  2sb8ev  2354  sbel2x  2474  2sb8e  2535  dfmo  2596  sb8eulem  2598  2mo2  2649  2eu7  2659  2eu8  2660  sbabel  2940  r19.26-3  3096  r19.23v  3207  rexcom  3281  ralcom13  3284  rexcom13  3285  2ralor  3294  cbvreuw  3365  cbvreu  3370  ceqsralt  3453  ceqsalv  3457  ceqsex2  3472  ceqsex2v  3473  ceqsex4v  3475  ralrab2  3629  rexrab2  3632  reu2  3655  rmo4  3660  reu8  3663  rmo3f  3664  2reu5lem3  3687  sbc3an  3782  sbcimdv  3786  reu8nf  3806  rmo2  3816  rmo3  3818  rmoanim  3823  dfss2OLD  3904  ss2rab  4000  rabss  4001  ssrab  4002  dfdif3  4045  symdifass  4182  dfss4  4189  undi  4205  indifdi  4214  undif3  4221  difin2  4222  difin0ss  4299  ab0OLD  4306  disj  4378  disjOLD  4379  disj4  4389  rabsssn  4600  disjsn  4644  raldifsni  4725  ssunpr  4762  sspr  4763  sstp  4764  uni0b  4864  uni0c  4865  ssint  4892  intprg  4909  iunssf  4970  iunss  4971  iundif2  4999  disjor  5050  nfnid  5293  reusv2lem4  5319  ssextss  5363  exss  5372  eqvinop  5395  sbcop  5397  opcom  5409  opeqpr  5413  brabsb  5437  opelopabf  5451  dfid3  5483  pofun  5512  opeliunxp  5645  xpiundi  5648  brinxp2  5655  reliun  5715  exopxfr  5741  cnvuni  5784  dmopab3  5817  rnep  5825  elres  5919  elsnres  5920  elrid  5942  asymref2  6011  intirr  6012  xpeq0  6052  xpdifid  6060  ssrnres  6070  dminxp  6072  dfrel4v  6082  elid  6091  dmsnn0  6099  rnco  6145  coeq0  6148  resssxp  6162  dfpo2  6188  sspred  6200  frpoind  6230  wfiOLD  6239  sb8iota  6388  dffun2  6428  fun11  6492  isarep1  6506  dff1o4  6708  opabiota  6833  fvopab5  6889  eqfnfv3  6893  fvn0ssdmfun  6934  fnressn  7012  f13dfv  7127  dff1o6  7128  fliftel  7160  oprabidw  7286  oprabid  7287  eloprabga  7360  mpo2eqb  7384  ralrnmpo  7390  uniuni  7590  dflim3  7669  dfom2  7689  elxp4  7743  elxp5  7744  opabex3d  7781  opabex3rd  7782  opabex3  7783  el2xptp  7850  fsplit  7928  xporderlem  7939  dfrecs3  8174  dfrecs3OLD  8175  tz7.48lem  8242  seqomlem2  8252  oaord  8340  oeeu  8396  nnaord  8412  ecid  8529  mptelixpg  8681  elixpsn  8683  xpsnen  8796  xpcomco  8802  xpassen  8806  omxpenlem  8813  dom0  8841  modom  8953  frind  9439  tz9.12lem3  9478  rankxpsuc  9571  cp  9580  cardprclem  9668  infxpenlem  9700  dfac5lem1  9810  dfac5lem2  9811  dfac5lem5  9814  dfac10c  9825  kmlem3  9839  kmlem12  9848  kmlem13  9849  kmlem14  9850  kmlem15  9851  ackbij2  9930  cf0  9938  cflim2  9950  dffin7-2  10085  dfacfin7  10086  fin1a2lem12  10098  axdc3lem3  10139  cfpwsdom  10271  recmulnq  10651  genpass  10696  psslinpr  10718  suplem2pr  10740  opelreal  10817  ltxrlt  10976  addid1  11085  elnn0  12165  elxnn0  12237  elnn0z  12262  nnwos  12584  elxr  12781  xrnepnf  12783  elfzuzb  13179  4fvwrd4  13305  preduz  13307  elfzo2  13319  ssnn0fi  13633  sqeqori  13858  xpcogend  14613  cotr2g  14615  fsumcom2  15414  modfsummod  15434  fprodcom2  15622  rpnnen2lem12  15862  gcdcllem1  16134  isprm2  16315  isprm7  16341  pythagtriplem2  16446  infpn2  16542  4sqlem12  16585  initoid  17632  termoid  17633  eldmcoa  17696  oduposb  17962  gsumwspan  18400  smndex1basss  18459  smndex1mgm  18461  isnsg2  18699  isnsg4  18710  cycsubmel  18734  efgcpbllemb  19276  dmdprd  19516  dprdval  19521  dprdw  19528  dprd2d2  19562  dfrhm2  19876  brric2  19904  issubrg  19939  islmim  20239  lbsextlem2  20336  cnfldfunALT  20523  pjfval2  20826  opsrtoslem1  21172  ntreq0  22136  cmpcov2  22449  cmpsub  22459  2ndcdisj  22515  unisngl  22586  txbas  22626  elpt  22631  txkgen  22711  xkococn  22719  fbun  22899  trfil2  22946  fin1aufil  22991  alexsubALTlem3  23108  cnextcn  23126  qustgplem  23180  eltsms  23192  ustn0  23280  fmucndlem  23351  metrest  23586  restmetu  23632  isclmp  24166  srabn  24429  ellogdm  25699  1cubr  25897  leibpilem2  25996  dmarea  26012  vmasum  26269  dchrelbas2  26290  2lgslem4  26459  tgcgr4  26796  ltgov  26862  axlowdimlem13  27225  axeuclidlem  27233  numedglnl  27417  nbupgrres  27634  vtxd0nedgb  27758  rusgrprc  27860  usgr2pth0  28034  wspthsnwspthsnon  28182  isclwwlk  28249  clwwlkn1  28306  clwwlkn2  28309  clwwlknonel  28360  3pthdlem1  28429  iseupthf1o  28467  frgr3v  28540  fusgr2wsp2nb  28599  frgrregord013  28660  h2hcau  29242  h2hlm  29243  shlesb1i  29649  shne0i  29711  chnlei  29748  cmbr2i  29859  pjneli  29986  ho02i  30092  adjsym  30096  adjeu  30152  lnopeqi  30271  largei  30530  atoml2i  30646  cdj3lem3b  30703  or3di  30711  mo5f  30738  dmrab  30745  disjnf  30810  disjorf  30819  ssrelf  30856  ofpreima  30904  disjdsct  30937  1stpreima  30941  2ndpreima  30942  f1od2  30958  xrdifh  31003  nndiffz1  31009  prmidl0  31528  zarclsun  31722  ordtconnlem1  31776  ind1a  31887  measiuns  32085  elunirnmbfm  32120  eulerpartlemr  32241  eulerpartlemgh  32245  eulerpartlemn  32248  ballotlemodife  32364  bnj250  32580  bnj334  32592  bnj345  32593  bnj89  32600  bnj115  32604  bnj919  32647  bnj1304  32699  bnj92  32742  bnj124  32751  bnj126  32753  bnj154  32758  bnj155  32759  bnj523  32767  bnj526  32768  bnj540  32772  bnj581  32788  bnj916  32813  bnj929  32816  bnj964  32823  bnj978  32829  bnj983  32831  bnj1039  32851  bnj1040  32852  bnj1123  32866  bnj1128  32870  bnj1398  32914  lfuhgr3  32981  cvmlift2lem1  33164  satfv0  33220  satf0  33234  satf0op  33239  satffunlem  33263  satffunlem1lem1  33264  satffunlem2lem1  33266  elmthm  33438  quad3  33528  3orit  33560  snres0  33577  ralxp3f  33588  brtp  33623  dftr6  33624  eldm3  33634  elrn3  33635  elima4  33656  19.12b  33683  brttrcl2  33700  ttrcltr  33702  rnttrcl  33708  frpoins3xpg  33714  poxp2  33717  nosupbnd1lem4  33841  nosupbnd2lem1  33845  slenlt  33882  madeval2  33964  made0  33984  brtxp  34109  brtxp2  34110  brpprod  34114  brpprod3a  34115  elfix  34132  dffix2  34134  ellimits  34139  sscoid  34142  dffun10  34143  elfuns  34144  elsingles  34147  brimg  34166  brapply  34167  brsuccf  34170  funpartlem  34171  brrestrict  34178  dfrecs2  34179  dfrdg4  34180  brlb  34184  altopthc  34200  altopthd  34201  fvtransport  34261  hfext  34412  nn0prpw  34439  filnetlem4  34497  df3nandALT2  34516  bj-sbeq  35013  bj-csbsnlem  35015  bj-elsngl  35085  bj-eltag  35094  bj-tagex  35104  bj-projun  35111  bj-reabeq  35144  bj-disj2r  35145  bj-restuni  35195  bj-elid6  35268  bj-eldiag  35274  bj-eldiag2  35275  topdifinffinlem  35445  relowlpssretop  35462  fvineqsneq  35510  wl-3xorbi  35571  wl-2mintru1  35588  wl-df3maxtru1  35590  wl-dfclab  35674  phpreu  35688  poimirlem24  35728  poimirlem26  35730  poimirlem30  35734  areacirclem5  35796  isbnd2  35868  sbcalf  36199  sbcexf  36200  sbccom2  36210  sbccom2f  36211  sbccom2fi  36212  csbcom2fi  36213  anan  36306  idinxpssinxp2  36380  ineleq  36413  brabidgaw  36422  brabidga  36423  inxpxrn  36448  rnxrn  36451  cossssid2  36513  cossssid3  36514  cosscnvssid3  36521  dfeldisj3  36757  dfeldisj4  36758  prtlem70  36798  prtlem16  36810  ishlat2  37294  pmapglb  37711  polval2N  37847  dicelval3  39121  mapdordlem1a  39575  isdomn5  40099  prjspeclsp  40372  fz1eqin  40507  7rexfrabdioph  40538  rmydioph  40752  dford4  40767  areaquad  40963  ifpan23  40965  ifpdfnan  40991  ifpdfxor  40992  ifpidg  40996  ifpid1g  40999  ifpim123g  41005  ifp1bi  41007  ifpimimb  41009  ifpororb  41010  ifpbibib  41015  rp-fakeuninass  41021  dfsucon  41028  cllem0  41062  rababg  41070  elmapintrab  41073  elmapintab  41093  undmrnresiss  41101  ss2iundf  41156  dfxor4  41263  dfhe3  41272  dffrege115  41475  frege131  41491  frege133  41493  clsk1indlem4  41543  clsk1indlem1  41544  expandrexn  41798  rr-groth  41806  rr-grothshortbi  41810  undisjrab  41813  pm13.196a  41921  eelT11  42216  eelTT1  42219  eelT01  42220  eel0T1  42221  uunTT1  42302  uunTT1p1  42303  uunTT1p2  42304  uunT11  42305  uunT11p1  42306  uunT11p2  42307  uun111  42314  ssrabf  42553  rabssf  42557  disjinfi  42620  elicores  42961  fourierdlem42  43580  iundjiun  43888  2reu7  44490  2reu8  44491  2reu8i  44492  dfdfat2  44507  aovov0bi  44575  afv2orxorb  44607  afv2ndeffv0  44639  ichcircshi  44794  ichan  44795  icheq  44802  ichal  44806  prpair  44841  prproropf1olem0  44842  257prm  44901  fmtno4prmfac  44912  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  uspgrsprf1  45197  opeliun2xp  45556  rrx2xpref1o  45952  isthincd2  46207  aacllem  46391