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  337  pm5.32  572  biadan  817  orbi1i  911  orass  919  or32  923  cases  1040  dn1  1055  3anidm  1101  an33rean  1479  nanbi  1493  excxor  1509  cadan  1602  cadcomb  1606  nic-axALT  1668  tbw-bijust  1692  rb-bijust  1743  nf2  1779  19.43  1877  19.43OLD  1878  3exdistr  1956  19.12vvv  1984  excom13  2153  sbcom2  2162  sbco4  2164  sbn  2269  sbnf  2301  19.12vv  2337  eeeanv  2340  ee4anv  2341  2sb8ef  2346  sbel2x  2467  2sb8e  2523  dfmo  2584  sb8eulem  2586  2mo2  2635  2eu7  2646  2eu8  2647  sbabel  2927  r19.23v  3172  2ralor  3218  rexcomOLD  3278  ralcom13OLD  3282  rexcom13  3283  cbvreuwOLD  3398  cbvreu  3410  rabrabi  3437  cgsex4g  3509  ceqsex2  3519  ceqsex2v  3520  ceqsex3v  3521  ceqsex4v  3522  ceqsex6v  3523  ceqsex8v  3524  ralrab2  3690  rexrab2  3692  reu2  3717  rmo4  3722  reu8  3725  rmo3f  3726  2reu5lem3  3749  sbcimdv  3847  reu8nf  3867  rmo2  3877  rmo3  3879  rmoanim  3884  ss2rab  4064  rabss  4065  ssrab  4066  dfdif3  4110  symdifass  4250  dfss4  4257  undi  4273  indifdi  4282  undif3  4289  reuun2  4314  difin0ss  4370  ab0OLD  4377  disj  4449  disjOLD  4450  disj4  4460  rabsssn  4672  disjsn  4717  snssb  4788  raldifsni  4800  ssunpr  4837  sspr  4838  sstp  4839  uni0b  4937  uni0c  4938  ssint  4968  intprg  4985  iunssf  5048  iunss  5049  iundif2  5078  disjor  5129  nfnid  5375  reusv2lem4  5401  ssextss  5455  exss  5465  eqvinop  5489  sbcop  5491  opcom  5503  opeqpr  5507  brtp  5525  brabsb  5533  opelopabf  5547  dfid3  5579  pofun  5608  opeliunxp  5745  xpiundi  5748  brinxp2  5755  reliun  5818  exopxfr  5846  cnvuni  5889  dmopab3  5922  rnep  5929  elres  6025  elsnres  6026  elrid  6050  cnvsym  6119  cnvsymOLD  6120  asymref2  6124  intirr  6125  cnvopab  6144  xpeq0  6166  difxp  6170  xpdifid  6174  ssrnres  6184  dminxp  6186  dfrel4v  6196  elid  6205  dmsnn0  6213  imaco  6257  rnco  6258  coeq0  6261  resssxp  6276  dfpo2  6302  snres0  6304  sspred  6316  frpoind  6350  wfiOLD  6359  sb8iota  6513  dffun2OLDOLD  6561  fun11  6628  isarep1  6643  isarep1OLD  6644  dff1o4  6846  opabiota  6980  fvopab5  7037  eqfnfv3  7041  fvn0ssdmfun  7083  fnressn  7167  f13dfv  7283  dff1o6  7284  fliftel  7316  oprabidw  7450  oprabid  7451  eloprabga  7528  mpo2eqb  7553  ralrnmpo  7560  uniuni  7765  dflim3  7852  dfom2  7873  elxp4  7930  elxp5  7931  opabex3d  7970  opabex3rd  7971  opabex3  7972  el2xptp  8040  fsplit  8122  xporderlem  8132  ralxp3f  8142  frpoins3xpg  8145  poxp2  8148  suppvalbr  8169  dfrecs3  8393  dfrecs3OLD  8394  tz7.48lem  8462  seqomlem2  8472  oaord  8568  oeeu  8624  nnaord  8640  ecid  8801  mptelixpg  8954  elixpsn  8956  xpsnen  9080  xpcomco  9087  xpassen  9091  omxpenlem  9098  dom0OLD  9128  modom  9269  brttrcl2  9739  ttrcltr  9741  rnttrcl  9747  frind  9775  tz9.12lem3  9814  rankxpsuc  9907  cp  9916  cardprclem  10004  infxpenlem  10038  dfac5lem1  10148  dfac5lem2  10149  dfac5lem5  10152  dfac10c  10163  kmlem3  10177  kmlem12  10186  kmlem13  10187  kmlem14  10188  kmlem15  10189  ackbij2  10268  cf0  10276  cflim2  10288  dffin7-2  10423  dfacfin7  10424  fin1a2lem12  10436  axdc3lem3  10477  cfpwsdom  10609  recmulnq  10989  genpass  11034  psslinpr  11056  suplem2pr  11078  opelreal  11155  ltxrlt  11316  addrid  11426  elnn0  12507  elxnn0  12579  elnn0z  12604  nnwos  12932  elxr  13131  xrnepnf  13133  elfzuzb  13530  4fvwrd4  13656  preduz  13658  elfzo2  13670  ssnn0fi  13986  sqeqori  14213  xpcogend  14957  cotr2g  14959  fsumcom2  15756  modfsummod  15776  fprodcom2  15964  rpnnen2lem12  16205  gcdcllem1  16477  isprm2  16656  isprm7  16682  pythagtriplem2  16789  infpn2  16885  4sqlem12  16928  initoid  17993  termoid  17994  eldmcoa  18057  oduposb  18324  gsumwspan  18806  smndex1basss  18865  smndex1mgm  18867  isnsg2  19119  isnsg4  19130  cycsubmel  19163  efgcpbllemb  19722  dmdprd  19967  dprdval  19972  dprdw  19979  dprd2d2  20013  dfrhm2  20425  brric2  20457  issubrg  20522  islmim  20959  lbsextlem2  21059  isdomn5  21266  cnfldfun  21310  cnfldfunOLD  21323  pzriprnglem3  21426  pjfval2  21660  opsrtoslem1  22021  ntreq0  23025  cmpcov2  23338  cmpsub  23348  2ndcdisj  23404  unisngl  23475  txbas  23515  elpt  23520  txkgen  23600  xkococn  23608  fbun  23788  trfil2  23835  fin1aufil  23880  alexsubALTlem3  23997  cnextcn  24015  qustgplem  24069  eltsms  24081  ustn0  24169  fmucndlem  24240  metrest  24477  restmetu  24523  isclmp  25068  srabn  25332  ellogdm  26618  1cubr  26819  leibpilem2  26918  dmarea  26934  vmasum  27194  dchrelbas2  27215  2lgslem4  27384  nosupbnd1lem4  27690  nosupbnd2lem1  27694  slenlt  27731  madeval2  27826  made0  27846  tgcgr4  28407  ltgov  28473  axlowdimlem13  28837  axeuclidlem  28845  numedglnl  29029  nbupgrres  29249  vtxd0nedgb  29374  rusgrprc  29476  usgr2pth0  29651  wspthsnwspthsnon  29799  isclwwlk  29866  clwwlkn1  29923  clwwlkn2  29926  clwwlknonel  29977  3pthdlem1  30046  iseupthf1o  30084  frgr3v  30157  fusgr2wsp2nb  30216  frgrregord013  30277  h2hcau  30861  h2hlm  30862  shlesb1i  31268  shne0i  31330  chnlei  31367  cmbr2i  31478  pjneli  31605  ho02i  31711  adjsym  31715  adjeu  31771  lnopeqi  31890  largei  32149  atoml2i  32265  cdj3lem3b  32322  or3di  32337  mo5f  32365  dmrab  32373  disjnf  32439  disjorf  32448  ssrelf  32484  ofpreima  32532  disjdsct  32564  1stpreima  32568  2ndpreima  32569  f1od2  32585  xrdifh  32630  nndiffz1  32636  prmidl0  33262  zarclsun  33602  ordtconnlem1  33656  ind1a  33769  measiuns  33967  elunirnmbfm  34002  eulerpartlemr  34125  eulerpartlemgh  34129  eulerpartlemn  34132  ballotlemodife  34248  bnj250  34463  bnj334  34475  bnj345  34476  bnj89  34483  bnj115  34487  bnj919  34529  bnj1304  34581  bnj92  34624  bnj124  34633  bnj126  34635  bnj154  34640  bnj155  34641  bnj523  34649  bnj526  34650  bnj540  34654  bnj581  34670  bnj916  34695  bnj929  34698  bnj964  34705  bnj978  34711  bnj983  34713  bnj1039  34733  bnj1040  34734  bnj1123  34748  bnj1128  34752  bnj1398  34796  lfuhgr3  34860  cvmlift2lem1  35043  satfv0  35099  satf0  35113  satf0op  35118  satffunlem  35142  satffunlem1lem1  35143  satffunlem2lem1  35145  elmthm  35317  quad3  35405  3orit  35441  dftr6  35476  eldm3  35486  elrn3  35487  elima4  35502  19.12b  35528  brtxp  35607  brtxp2  35608  brpprod  35612  brpprod3a  35613  elfix  35630  dffix2  35632  ellimits  35637  sscoid  35640  dffun10  35641  elfuns  35642  elsingles  35645  brimg  35664  brapply  35665  brsuccf  35668  funpartlem  35669  brrestrict  35676  dfrecs2  35677  dfrdg4  35678  brlb  35682  altopthc  35698  altopthd  35699  fvtransport  35759  hfext  35910  nn0prpw  35938  filnetlem4  35996  df3nandALT2  36015  bj-sbeq  36510  bj-csbsnlem  36512  bj-elsngl  36578  bj-eltag  36587  bj-tagex  36597  bj-projun  36604  bj-reabeq  36637  bj-disj2r  36638  bj-restuni  36707  bj-elid6  36780  bj-eldiag  36786  bj-eldiag2  36787  topdifinffinlem  36957  relowlpssretop  36974  fvineqsneq  37022  wl-3xorbi  37083  wl-2mintru1  37100  wl-df3maxtru1  37102  wl-dfclab  37194  phpreu  37208  poimirlem24  37248  poimirlem26  37250  poimirlem30  37254  areacirclem5  37316  isbnd2  37387  sbcalf  37718  sbcexf  37719  sbccom2  37729  sbccom2f  37730  sbccom2fi  37731  csbcom2fi  37732  anan  37829  br1cnvinxp  37858  idinxpssinxp2  37920  ineleq  37956  brabidgaw  37967  brabidga  37968  inxpxrn  37997  rnxrn  38000  cossssid2  38070  cossssid3  38071  cosscnvssid3  38078  dfeldisj3  38321  dfeldisj4  38322  antisymrelres  38365  dfmembpart2  38372  mpet3  38438  cpet2  38439  prtlem70  38459  prtlem16  38471  ishlat2  38955  pmapglb  39373  polval2N  39509  dicelval3  40783  mapdordlem1a  41237  prjspeclsp  42171  sn-isghm  42232  abbibw  42237  fz1eqin  42331  7rexfrabdioph  42362  rmydioph  42577  dford4  42592  areaquad  42786  onsupmaxb  42809  onov0suclim  42845  nnoeomeqom  42883  tfsconcat0i  42916  faosnf0.11b  42999  ifpan23  43032  ifpdfnan  43058  ifpdfxor  43059  ifpidg  43063  ifpid1g  43066  ifpim123g  43072  ifp1bi  43074  ifpimimb  43076  ifpororb  43077  ifpbibib  43082  rp-fakeuninass  43088  dfsucon  43095  minregex  43106  cllem0  43138  rababg  43146  elmapintrab  43148  elmapintab  43168  undmrnresiss  43176  dfxor4  43338  dfhe3  43347  dffrege115  43550  frege131  43566  frege133  43568  clsk1indlem4  43616  clsk1indlem1  43617  expandrexn  43870  rr-groth  43878  rr-grothshortbi  43882  undisjrab  43885  pm13.196a  43993  eelT11  44288  eelTT1  44291  eelT01  44292  eel0T1  44293  uunTT1  44374  uunTT1p1  44375  uunTT1p2  44376  uunT11  44377  uunT11p1  44378  uunT11p2  44379  uun111  44386  ssrabf  44620  rabssf  44625  disjinfi  44704  elicores  45056  fourierdlem42  45675  iundjiun  45986  2reu7  46629  2reu8  46630  2reu8i  46631  dfdfat2  46646  aovov0bi  46714  afv2orxorb  46746  afv2ndeffv0  46778  ichcircshi  46931  ichan  46932  icheq  46939  ichal  46943  prpair  46978  prproropf1olem0  46979  257prm  47038  fmtno4prmfac  47049  nnsum4primeseven  47277  nnsum4primesevenALTV  47278  clnbgrel  47304  uspgrsprf1  47395  opeliun2xp  47582  rrx2xpref1o  47977  isthincd2  48230  aacllem  48420