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  1056  dn1  1071  3anidm  1119  an33rean  1511  nanbi  1527  excxor  1543  cadan  1636  cadcomb  1640  nic-axALT  1701  tbw-bijust  1725  rb-bijust  1776  nf2  1812  19.43  1909  19.43OLD  1910  3exdistr  1987  19.12vvv  2021  sbco4  2143  excom13  2205  sbcom2  2213  sbco4OLD  2215  sbn  2321  sbnf  2352  19.12vv  2385  eeeanv  2388  ee4anv  2389  ee4anvOLD  2390  2sb8ef  2394  sbel2x  2512  2sb8e  2568  dfmo2  2630  sb8eulem  2632  2mo2  2681  2eu7  2691  2eu8  2692  sbabel  2963  3r19.43  3140  r19.23v  3198  2ralor  3245  rexcom13  3304  cbvreu  3415  rabrabi  3442  cgsex4g  3509  ceqsex2  3513  ceqsex2v  3514  ceqsex3v  3515  ceqsex4v  3516  ceqsex6v  3517  ceqsex8v  3518  ralrab2  3670  rexrab2  3672  reu2  3697  rmo4  3702  reu8  3705  rmo3f  3706  2reu5lem3  3729  sbcimdv  3821  reu8nf  3839  rmo2  3849  rmo3  3851  rmoanim  3856  ss2rab  4031  rabss  4032  ssrab  4033  dfdif3OLD  4081  symdifass  4223  dfss4  4230  undi  4246  indifdi  4255  undif3  4261  reuun2  4286  difin0ss  4335  disj  4413  disj4  4422  rabsssn  4636  disjsn  4679  snssb  4750  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  5344  reusv2lem4  5370  ssextss  5432  exss  5442  eqvinop  5467  sbcop  5469  opcom  5482  opeqpr  5486  brtp  5505  brabsb  5513  opelopabf  5528  dfid3  5557  pofun  5585  opeliunxp  5726  opeliun2xp  5727  xpiundi  5730  brinxp2  5737  exopxfr  5827  cnvuni  5874  dmopab3  5907  rnep  5915  dmxp  5917  rnopab3  5944  elres  6017  elsnres  6018  elrid  6046  cnvsym  6112  asymref2  6115  intirr  6116  cnvopab  6135  xpeq0  6156  difxp  6160  xpdifid  6164  xpdifcnvepel  6165  ssrnres  6175  dminxp  6177  dfrel4v  6187  elid  6197  dmsnn0  6205  imaco  6249  rnco  6250  rncoOLD  6251  coeq0  6254  resssxp  6268  dfpo2  6294  snres0  6296  sspred  6308  frpoind  6340  sb8iota  6500  fun11  6607  isarep1  6622  dff1o4  6827  opabiota  6961  fvopab5  7021  eqfnfv3  7025  fvn0ssdmfun  7067  fnressn  7153  f13dfv  7270  dff1o6  7271  fliftel  7305  oprabidw  7439  oprabid  7440  eloprabga  7517  mpo2eqb  7540  ralrnmpo  7547  uniuni  7757  dflim3  7839  dfom2  7860  elxp4  7915  elxp5  7916  opabex3d  7958  opabex3rd  7959  opabex3  7960  el2xptp  8028  fsplit  8108  xporderlem  8119  ralxp3f  8129  frpoins3xpg  8132  poxp2  8135  suppvalbr  8156  dfrecs3  8355  tz7.48lem  8424  seqomlem2  8434  oaord  8528  oeeu  8585  nnaord  8601  ecid  8774  mptelixpg  8929  elixpsn  8931  xpsnen  9045  xpcomco  9051  xpassen  9055  omxpenlem  9062  modom  9207  brttrcl2  9679  ttrcltr  9681  rnttrcl  9687  frind  9718  tz9.12lem3  9757  rankxpsuc  9850  cp  9873  cardprclem  9961  infxpenlem  9993  dfac5lem1  10103  dfac5lem2  10104  dfac5lem5  10107  dfac10c  10118  kmlem3  10132  kmlem12  10141  kmlem13  10142  kmlem14  10143  kmlem15  10144  ackbij2  10221  cf0  10230  cflim2  10243  dffin7-2  10378  dfacfin7  10379  fin1a2lem12  10391  axdc3lem3  10432  cfpwsdom  10565  recmulnq  10945  genpass  10990  psslinpr  11012  suplem2pr  11034  opelreal  11111  ltxrlt  11276  addrid  11386  ind1a  12225  elnn0  12502  elxnn0  12575  elnn0z  12600  nnwos  12935  elxr  13137  xrnepnf  13139  elfzuzb  13542  4fvwrd4  13672  preduz  13674  elfzo2  13686  ssnn0fi  14017  sqeqori  14246  xpcogend  15007  cotr2g  15009  fsumcom2  15821  modfsummod  15842  fprodcom2  16034  rpnnen2lem12  16277  gcdcllem1  16553  isprm2  16736  isprm7  16763  pythagtriplem2  16873  infpn2  16969  4sqlem12  17012  initoid  18054  termoid  18055  eldmcoa  18118  oduposb  18379  gsumwspan  18901  smndex1basss  18963  smndex1mgm  18965  isnsg2  19218  isnsg4  19229  cycsubmel  19267  efgcpbllemb  19821  dmdprd  20066  dprdval  20071  dprdw  20078  dprd2d2  20112  dfrhm2  20552  brric2  20585  issubrg  20652  isdomn5  20791  islmim  21157  lbsextlem2  21257  prmidl0  21443  cnfldfun  21501  pzriprnglem3  21598  pjfval2  21824  opsrtoslem1  22171  ntreq0  23199  cmpcov2  23512  cmpsub  23522  2ndcdisj  23578  unisngl  23649  txbas  23689  elpt  23694  txkgen  23774  xkococn  23782  fbun  23962  trfil2  24009  fin1aufil  24054  alexsubALTlem3  24171  cnextcn  24189  qustgplem  24243  eltsms  24255  ustn0  24343  fmucndlem  24412  metrest  24646  restmetu  24692  isclmp  25221  srabn  25484  ellogdm  26766  1cubr  26969  leibpilem2  27068  dmarea  27084  vmasum  27342  dchrelbas2  27363  2lgslem4  27532  nosupbnd1lem4  27837  nosupbnd2lem1  27841  lenlts  27878  madeval2  27988  made0  28018  oniso  28426  onsfi  28511  tgcgr4  28762  ltgov  28828  plngrotlem2  29024  axlowdimlem13  29241  axeuclidlem  29249  numedglnl  29431  nbupgrres  29651  vtxd0nedgb  29775  rusgrprc  29877  usgr2pth0  30051  wspthsnwspthsnon  30202  isclwwlk  30272  clwwlkn1  30329  clwwlkn2  30332  clwwlknonel  30383  3pthdlem1  30452  iseupthf1o  30490  frgr3v  30563  fusgr2wsp2nb  30622  frgrregord013  30683  h2hcau  31268  h2hlm  31269  shlesb1i  31675  shne0i  31737  chnlei  31774  cmbr2i  31885  pjneli  32012  ho02i  32118  adjsym  32122  adjeu  32178  lnopeqi  32297  largei  32556  atoml2i  32672  cdj3lem3b  32729  or3di  32744  mo5f  32772  dmrab  32780  rabsspr  32784  rabsstp  32785  disjnf  32852  disjorf  32861  ssrelf  32897  ofpreima  32947  disjdsct  32985  1stpreima  32989  2ndpreima  32990  f1od2  33001  xrdifh  33062  nndiffz1  33068  domnprodeq0  33536  zarclsun  34201  ordtconnlem1  34255  measiuns  34548  elunirnmbfm  34583  eulerpartlemr  34705  eulerpartlemgh  34709  eulerpartlemn  34712  ballotlemodife  34829  bnj250  35031  bnj334  35043  bnj345  35044  bnj89  35051  bnj115  35055  bnj919  35097  bnj1304  35148  bnj92  35191  bnj124  35200  bnj126  35202  bnj154  35207  bnj155  35208  bnj523  35216  bnj526  35217  bnj540  35221  bnj581  35237  bnj916  35262  bnj929  35265  bnj964  35272  bnj978  35278  bnj983  35280  bnj1039  35300  bnj1040  35301  bnj1123  35315  bnj1128  35319  bnj1398  35363  lfuhgr3  35507  cvmlift2lem1  35689  satfv0  35745  satf0  35759  satf0op  35764  satffunlem  35788  satffunlem1lem1  35789  satffunlem2lem1  35791  elmthm  35963  quad3  36057  3orit  36103  dftr6  36138  eldm3  36148  elrn3  36149  elima4  36163  19.12b  36186  brtxp  36265  brtxp2  36266  brpprod  36270  brpprod3a  36271  elfix  36288  dffix2  36290  ellimits  36295  sscoid  36298  dffun10  36299  elfuns  36300  elsingles  36303  brimg  36322  brapply  36323  lemsuccf  36326  brsuccf  36327  funpartlem  36329  brrestrict  36336  dfrecs2  36337  dfrdg4  36338  brlb  36342  altopthc  36358  altopthd  36359  fvtransport  36419  hfext  36570  ss-ax8  36622  nn0prpw  36719  filnetlem4  36777  df3nandALT2  36796  regsfromregtco  36934  mh-prprimbi  36939  mh-regprimbi  36941  mh-infprim2bi  36943  mh-infprim3bi  36944  bj-sbeq  37421  bj-csbsnlem  37423  bj-elsngl  37488  bj-eltag  37497  bj-tagex  37507  bj-projun  37514  bj-reabeq  37547  bj-disj2r  37548  bj-axseprep  37594  bj-restuni  37622  bj-elid6  37697  bj-eldiag  37703  bj-eldiag2  37704  topdifinffinlem  37876  relowlpssretop  37893  fvineqsneq  37941  wl-3xorbi  38002  wl-2mintru1  38019  wl-df3maxtru1  38021  wl-dfclab  38123  phpreu  38138  poimirlem24  38178  poimirlem26  38180  poimirlem30  38184  areacirclem5  38246  isbnd2  38317  sbcalf  38648  sbcexf  38649  sbccom2  38659  sbccom2f  38660  sbccom2fi  38661  csbcom2fi  38662  anan  38769  br1cnvinxp  38793  idinxpssinxp2  38858  ineleq  38888  brabidgaw  38907  brabidga  38908  inxpxrn  38952  rnxrn  38955  dfsucmap3  38997  cossssid2  39092  cossssid3  39093  cosscnvssid3  39100  dfeldisj3  39345  dfeldisj4  39346  antisymrelres  39400  dfmembpart2  39407  mpet3  39484  cpet2  39485  prtlem70  39516  prtlem16  39528  ishlat2  40012  pmapglb  40429  polval2N  40565  dicelval3  41839  mapdordlem1a  42293  redvmptabs  43004  fimgmcyclem  43186  fimgmcyc  43187  prjspeclsp  43229  sn-isghm  43290  abbibw  43294  fz1eqin  43385  7rexfrabdioph  43412  rmydioph  43626  dford4  43641  areaquad  43828  onsupmaxb  43851  onov0suclim  43886  nnoeomeqom  43924  tfsconcat0i  43957  faosnf0.11b  44038  ifpan23  44071  ifpdfnan  44097  ifpdfxor  44098  ifpidg  44102  ifpid1g  44105  ifpim123g  44111  ifp1bi  44113  ifpimimb  44115  ifpororb  44116  ifpbibib  44121  rp-fakeuninass  44127  dfsucon  44134  minregex  44145  cllem0  44177  rababg  44185  elmapintrab  44187  elmapintab  44207  undmrnresiss  44215  dfxor4  44377  dfhe3  44386  dffrege115  44589  frege131  44605  frege133  44607  clsk1indlem4  44655  clsk1indlem1  44656  expandrexn  44886  rr-groth  44894  rr-grothshortbi  44898  undisjrab  44901  pm13.196a  45009  eelT11  45300  eelTT1  45303  eelT01  45304  eel0T1  45305  uunTT1  45386  uunTT1p1  45387  uunTT1p2  45388  uunT11  45389  uunT11p1  45390  uunT11p2  45391  uun111  45398  xpwf  45558  permaxinf2lem  45606  permac8prim  45608  ssrabf  45717  rabssf  45722  disjinfi  45795  elicores  46134  fourierdlem42  46748  iundjiun  47059  2reu7  47730  2reu8  47731  2reu8i  47732  dfdfat2  47747  aovov0bi  47815  afv2orxorb  47847  afv2ndeffv0  47879  ichcircshi  48085  ichan  48086  icheq  48093  ichal  48097  prpair  48132  prproropf1olem0  48133  257prm  48195  fmtno4prmfac  48206  nnsum4primeseven  48447  nnsum4primesevenALTV  48448  clnbgrel  48475  isubgr3stgrlem4  48616  usgrexmpl2nb1  48679  usgrexmpl2nb2  48680  gpgprismgr4cycllem10  48751  uspgrsprf1  48794  rrx2xpref1o  49376  iinxp  49487  resinsn  49528  resinsnALT  49529  0funcALT  49744  catcsect  50054  isthincd2  50093  aacllem  50457