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 ⊢ (𝜑 ↔ 𝜃)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi1i  341  pm5.32  584  biadan  831  orbi1i  927  orass  935  or32  939  cases  1058  dn1  1073  3anidm  1121  an33rean  1514  nanbi  1530  excxor  1546  cadan  1642  cadcomb  1646  nic-axALT  1707  tbw-bijust  1731  rb-bijust  1782  nf2  1818  19.43  1915  19.43OLD  1916  3exdistr  1993  19.12vvv  2027  sbco4  2140  excom13  2202  sbcom2  2210  sbco4OLD  2212  sbn  2318  sbnf  2349  19.12vv  2382  eeeanv  2385  ee4anv  2386  ee4anvOLD  2387  2sb8ef  2391  sbel2x  2509  2sb8e  2565  dfmo2  2627  sb8eulem  2629  2mo2  2678  2eu7  2688  2eu8  2689  sbabel  2960  3r19.43  3137  r19.23v  3195  2ralor  3242  rexcom13  3301  cbvreu  3411  rabrabi  3438  cgsex4g  3504  ceqsex2  3508  ceqsex2v  3509  ceqsex3v  3510  ceqsex4v  3511  ceqsex6v  3512  ceqsex8v  3513  ralrab2  3664  rexrab2  3666  reu2  3691  rmo4  3696  reu8  3699  rmo3f  3700  2reu5lem3  3723  sbcimdv  3815  reu8nf  3833  rmo2  3843  rmo3  3845  rmoanim  3851  ss2rab  4026  rabss  4027  ssrab  4028  dfdif3OLD  4076  symdifass  4218  dfss4  4225  undi  4241  indifdi  4250  undif3  4256  reuun2  4281  difin0ss  4331  disj  4413  disj4  4422  rabsssn  4639  disjsn  4682  snssb  4753  raldifsni  4768  ssunpr  4804  sspr  4805  sstp  4806  uni0b  4904  uni0c  4905  ssint  4934  intprg  4951  iunssf  5012  iunssfOLD  5013  iunss  5014  iunssOLD  5015  iundif2  5043  disjor  5096  nfnid  5351  reusv2lem4  5377  ssextss  5439  exss  5449  eqvinop  5474  sbcop  5476  opcom  5489  opeqpr  5493  brtp  5512  brabsb  5520  opelopabf  5535  dfid3  5564  pofun  5592  opeliunxp  5733  opeliun2xp  5734  xpiundi  5737  brinxp2  5744  exopxfr  5834  cnvuni  5881  dmopab3  5914  rnep  5922  dmxp  5924  rnopab3  5951  elres  6024  elsnres  6025  elrid  6053  cnvsym  6119  asymref2  6122  intirr  6123  cnvopab  6142  xpeq0  6162  difxp  6166  xpdifid  6170  xpdifcnvepel  6171  ssrnres  6181  dminxp  6183  dfrel4v  6193  elid  6203  dmsnn0  6213  imaco  6257  rnco  6258  rncoOLD  6259  coeq0  6262  resssxp  6277  dfpo2  6304  snres0  6306  sspred  6318  frpoind  6350  sb8iota  6510  fun11  6617  isarep1  6631  dff1o4  6836  opabiota  6970  fvopab5  7030  eqfnfv3  7034  fvn0ssdmfun  7076  fnressn  7162  f13dfv  7283  dff1o6  7284  fliftel  7318  oprabidw  7454  oprabid  7455  eloprabga  7532  mpo2eqb  7555  ralrnmpo  7562  uniuni  7770  dflim3  7852  dfom2  7873  elxp4  7928  elxp5  7929  opabex3d  7971  opabex3rd  7972  opabex3  7973  el2xptp  8041  fsplit  8121  xporderlem  8132  ralxp3f  8142  frpoins3xpg  8145  poxp2  8148  suppvalbr  8169  dfrecs3  8368  tz7.48lem  8437  seqomlem2  8447  oaord  8541  oeeu  8598  nnaord  8614  ecid  8787  mptelixpg  8942  elixpsn  8944  xpsnen  9059  xpcomco  9065  xpassen  9069  omxpenlem  9076  modom  9221  brttrcl2  9693  ttrcltr  9695  rnttrcl  9701  frind  9732  tz9.12lem3  9771  rankxpsuc  9864  cp  9893  cardprclem  9984  infxpenlem  10016  dfac5lem1  10126  dfac5lem2  10127  dfac5lem5  10130  dfac10c  10141  kmlem3  10155  kmlem12  10164  kmlem13  10165  kmlem14  10166  kmlem15  10167  ackbij2  10244  cf0  10252  cflim2  10265  dffin7-2  10400  dfacfin7  10401  fin1a2lem12  10413  axdc3lem3  10454  cfpwsdom  10587  recmulnq  10967  genpass  11012  psslinpr  11034  suplem2pr  11056  opelreal  11133  ltxrlt  11298  addrid  11408  ind1a  12247  elnn0  12524  elxnn0  12597  elnn0z  12622  nnwos  12957  elxr  13159  xrnepnf  13161  elfzuzb  13564  4fvwrd4  13695  preduz  13697  elfzo2  13709  ssnn0fi  14041  sqeqori  14270  xpcogend  15037  cotr2g  15039  fsumcom2  15851  modfsummod  15872  fprodcom2  16064  rpnnen2lem12  16306  gcdcllem1  16582  isprm2  16765  isprm7  16792  pythagtriplem2  16902  infpn2  16998  4sqlem12  17041  initoid  18083  termoid  18084  eldmcoa  18147  oduposb  18408  gsumwspan  18936  smndex1basss  18998  smndex1mgm  19000  isnsg2  19253  isnsg4  19264  cycsubmel  19302  efgcpbllemb  19856  dmdprd  20101  dprdval  20106  dprdw  20113  dprd2d2  20147  dfrhm2  20589  isbrric2  20638  issubrg  20707  isdomn5  20846  islmim  21220  lbsextlem2  21320  prmidl0  21515  cnfldfun  21573  pzriprnglem3  21670  pjfval2  21896  opsrtoslem1  22243  ntreq0  23271  cmpcov2  23584  cmpsub  23594  2ndcdisj  23650  unisngl  23721  txbas  23761  elpt  23766  txkgen  23846  xkococn  23854  fbun  24034  trfil2  24081  fin1aufil  24126  alexsubALTlem3  24243  cnextcn  24261  qustgplem  24315  eltsms  24327  ustn0  24415  fmucndlem  24484  metrest  24718  restmetu  24764  isclmp  25293  srabn  25556  ellogdm  26841  1cubr  27044  leibpilem2  27143  dmarea  27159  vmasum  27417  dchrelbas2  27438  2lgslem4  27607  nosupbnd1lem4  27912  nosupbnd2lem1  27916  lenlts  27953  madeval2  28063  made0  28093  oniso  28501  onsfi  28586  tgcgr4  28837  ltgov  28903  plngrotlem2  29107  axlowdimlem13  29341  axeuclidlem  29349  numedglnl  29531  nbupgrres  29751  vtxd0nedgb  29875  rusgrprc  29977  usgr2pth0  30151  wspthsnwspthsnon  30302  isclwwlk  30372  clwwlkn1  30429  clwwlkn2  30432  clwwlknonel  30483  3pthdlem1  30552  iseupthf1o  30590  frgr3v  30663  fusgr2wsp2nb  30722  frgrregord013  30783  h2hcau  31368  h2hlm  31369  shlesb1i  31775  shne0i  31837  chnlei  31874  cmbr2i  31985  pjneli  32112  ho02i  32218  adjsym  32222  adjeu  32278  lnopeqi  32397  largei  32656  atoml2i  32772  cdj3lem3b  32829  or3di  32844  mo5f  32872  dmrab  32880  rabsspr  32884  rabsstp  32885  disjnf  32952  disjorf  32961  ssrelf  32997  ofpreima  33047  disjdsct  33085  1stpreima  33089  2ndpreima  33090  f1od2  33101  xrdifh  33162  nndiffz1  33168  domnprodeq0  33630  zarclsun  34291  ordtconnlem1  34345  measiuns  34639  elunirnmbfm  34674  eulerpartlemr  34796  eulerpartlemgh  34800  eulerpartlemn  34803  ballotlemodife  34920  bnj250  35122  bnj334  35134  bnj345  35135  bnj89  35142  bnj115  35146  bnj919  35188  bnj1304  35239  bnj92  35282  bnj124  35291  bnj126  35293  bnj154  35298  bnj155  35299  bnj523  35307  bnj526  35308  bnj540  35312  bnj581  35328  bnj916  35353  bnj929  35356  bnj964  35363  bnj978  35369  bnj983  35371  bnj1039  35391  bnj1040  35392  bnj1123  35406  bnj1128  35410  bnj1398  35454  lfuhgr3  35633  cvmlift2lem1  35815  satfv0  35871  satf0  35885  satf0op  35890  satffunlem  35914  satffunlem1lem1  35915  satffunlem2lem1  35917  elmthm  36089  quad3  36183  3orit  36229  dftr6  36264  eldm3  36274  elrn3  36275  elima4  36289  19.12b  36312  brtxp  36391  brtxp2  36392  brpprod  36396  brpprod3a  36397  elfix  36414  dffix2  36416  ellimits  36421  sscoid  36424  dffun10  36425  elfuns  36426  elsingles  36429  brimg  36448  brapply  36449  lemsuccf  36452  brsuccf  36453  funpartlem  36455  brrestrict  36462  dfrecs2  36463  dfrdg4  36464  brlb  36468  altopthc  36484  altopthd  36485  fvtransport  36545  hfext  36696  ss-ax8  36778  nn0prpw  36875  filnetlem4  36933  df3nandALT2  36952  regsfromregtco  37090  mh-prprimbi  37095  mh-regprimbi  37097  mh-infprim2bi  37099  mh-infprim3bi  37100  bj-sbeq  37577  bj-csbsnlem  37579  bj-elsngl  37645  bj-eltag  37654  bj-tagex  37664  bj-projun  37671  bj-reabeq  37704  bj-disj2r  37705  bj-axseprep  37752  bj-restuni  37780  bj-elid6  37855  bj-eldiag  37861  bj-eldiag2  37862  topdifinffinlem  38034  relowlpssretop  38051  fvineqsneq  38099  wl-3xorbi  38160  wl-2mintru1  38177  wl-df3maxtru1  38179  wl-dfclab  38281  phpreu  38296  poimirlem24  38336  poimirlem26  38338  poimirlem30  38342  areacirclem5  38404  isbnd2  38475  sbcalf  38804  sbcexf  38805  sbccom2  38815  sbccom2f  38816  sbccom2fi  38817  csbcom2fi  38818  anan  38925  br1cnvinxp  38949  idinxpssinxp2  39014  ineleq  39044  brabidgaw  39063  brabidga  39064  inxpxrn  39108  rnxrn  39111  dfsucmap3  39153  cossssid2  39248  cossssid3  39249  cosscnvssid3  39256  dfeldisj3  39501  dfeldisj4  39502  antisymrelres  39556  dfmembpart2  39563  mpet3  39640  cpet2  39641  prtlem70  39672  prtlem16  39684  ishlat2  40168  pmapglb  40585  polval2N  40721  dicelval3  41995  mapdordlem1a  42449  redvmptabs  43162  fimgmcyclem  43342  fimgmcyc  43343  prjspeclsp  43385  sn-isghm  43446  abbibw  43450  fz1eqin  43541  7rexfrabdioph  43568  rmydioph  43782  dford4  43797  areaquad  43984  onsupmaxb  44007  onov0suclim  44042  nnoeomeqom  44080  tfsconcat0i  44113  faosnf0.11b  44194  ifpan23  44227  ifpdfnan  44253  ifpdfxor  44254  ifpidg  44258  ifpid1g  44261  ifpim123g  44267  ifp1bi  44269  ifpimimb  44271  ifpororb  44272  ifpbibib  44277  rp-fakeuninass  44283  dfsucon  44290  minregex  44301  cllem0  44333  rababg  44341  elmapintrab  44343  elmapintab  44363  undmrnresiss  44371  dfxor4  44533  dfhe3  44542  dffrege115  44745  frege131  44761  frege133  44763  clsk1indlem4  44811  clsk1indlem1  44812  expandrexn  45042  rr-groth  45050  rr-grothshortbi  45054  undisjrab  45057  pm13.196a  45165  eelT11  45456  eelTT1  45459  eelT01  45460  eel0T1  45461  uunTT1  45542  uunTT1p1  45543  uunTT1p2  45544  uunT11  45545  uunT11p1  45546  uunT11p2  45547  uun111  45554  xpwf  45714  permaxinf2lem  45762  permac8prim  45764  ssrabf  45873  rabssf  45878  disjinfi  45951  elicores  46290  fourierdlem42  46904  iundjiun  47215  2reu7  47889  2reu8  47890  2reu8i  47891  dfdfat2  47906  aovov0bi  47974  afv2orxorb  48006  afv2ndeffv0  48038  ichcircshi  48244  ichan  48245  icheq  48252  ichal  48256  prpair  48291  prproropf1olem0  48292  257prm  48354  fmtno4prmfac  48365  nnsum4primeseven  48606  nnsum4primesevenALTV  48607  clnbgrel  48634  isubgr3stgrlem4  48775  usgrexmpl2nb1  48838  usgrexmpl2nb2  48839  gpgprismgr4cycllem10  48910  uspgrsprf1  48953  rrx2xpref1o  49539  iinxp  49650  resinsn  49691  resinsnALT  49692  0funcALT  49907  catcsect  50217  isthincd2  50256  alsanmo  50629  ralsanmo  50630  aacllem  50662