Theorem 3bitrd 306

Description: Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.)

Hypotheses

Ref	Expression
3bitrd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitrd.2	⊢ (𝜑 → (𝜒 ↔ 𝜃))
3bitrd.3	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
3bitrd	⊢ (𝜑 → (𝜓 ↔ 𝜏))

Proof of Theorem 3bitrd

Step	Hyp	Ref	Expression
1		3bitrd.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		3bitrd.2	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
3	1, 2	bitrd 280	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitrd.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 280	1 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  2reu4lem  4451  elimhyp3v  4522  elimhyp4v  4523  keephyp3v  4528  ralsng  4607  opeqsng  5444  snopeqop  5447  frsn  5706  f1eq123d  6759  foeq123d  6760  f1oeq123d  6761  fnmptfvd  6982  fnotovb  7408  ofrfvalg  7628  eloprabi  8005  fnmpoovd  8026  suppsnop  8118  smoeq  8280  naddasslem1  8620  naddasslem2  8621  mapsnend  8973  infglbb  9395  wemapwe  9609  fseqenlem1  9937  dfac12lem2  10058  fin23lem22  10240  pwfseqlem5  10577  pwfseq  10578  enqbreq2  10834  lterpq  10884  ltdiv23  12038  lediv23  12039  negfi  12096  halfpos  12398  addltmul  12404  div4p1lem1div2  12423  supminf  12876  supxrbnd1  13264  supxrbnd2  13265  iccf1o  13440  fzshftral  13560  fzoshftral  13733  2tnp1ge0ge0  13779  dfceil2  13789  modirr  13895  hashen1  14323  seqcoll  14417  hash2prb  14425  hashle2prv  14431  hash3tpb  14448  s111  14569  swrdspsleq  14619  pfxnd0  14642  pfxeq  14649  wrd2ind  14676  2swrd2eqwrdeq  14906  eqwrds3  14914  limsupgle  15430  tanaddlem  16124  difmod0  16247  dvdssub  16264  addmodlteqALT  16285  dvdsmod  16289  oddp1even  16304  nn0o1gt2  16341  nn0oddm1d2  16345  bitscmp  16398  saddisjlem  16424  smueqlem  16450  ncoprmgcdne1b  16610  cncongr1  16627  cncongr2  16628  prmreclem5  16882  4sqlem11  16917  4sqlem17  16923  vdwmc2  16941  ismre  17543  acsfn  17616  dfiso2  17730  brcic  17756  isssc  17778  setcinv  18048  cat1  18055  intopsn  18613  sgrp1  18688  sgrppropd  18690  sgrp2nmndlem4  18890  nmzsubg  19131  eqg0subg  19162  conjnmzb  19219  gsmsymgreqlem2  19397  symgfixels  19400  f1omvdconj  19412  oddvdsnn0  19510  oddvds  19513  odcong  19515  odf1  19528  dpjeq  20027  pgpfac1lem2  20043  isomnd  20089  ogrpinvlt  20110  ring1  20282  rngcinv  20609  ringcinv  20643  lsmspsn  21074  lbsacsbs  21149  rngqiprngimf1lem  21287  lpigen  21328  prmirredlem  21447  znf1o  21526  znleval  21529  znunit  21538  islinds2  21788  islindf4  21813  psdmul  22154  scmatf1  22514  isclo  23070  maxlp  23130  1stccn  23446  xkoinjcn  23670  elmptrab  23810  fbunfip  23852  elfm  23930  fmid  23943  flfnei  23974  isflf  23976  isfcls  23992  fclsopn  23997  isfcf  24017  cnextfun  24047  eltsms  24116  prdsxmetlem  24351  elmopn  24425  metss  24491  comet  24496  elbl4  24546  metuel2  24548  nrmmetd  24557  metdsge  24833  tcphcph  25222  fmcfil  25257  cmscsscms  25358  rrxmet  25393  minveclem4  25417  shft2rab  25493  sca2rab  25497  volsup2  25590  mbfsup  25649  i1fmullem  25679  mbfi1fseqlem4  25703  xrge0f  25716  itg2monolem1  25735  ellimc2  25862  cnlimc  25873  mdegleb  26047  r1pid2  26145  facth1  26150  ulm2  26368  sineq0  26506  coseq1  26507  efeq1  26510  sinord  26516  root1eq1  26737  angrtmuld  26790  affineequiv3  26807  quad2  26821  dcubic  26828  cubic2  26830  dquartlem1  26833  dquart  26835  quart  26843  rlimcnp  26947  lgamucov  27019  mumullem2  27161  chtub  27193  fsumvma  27194  fsumvma2  27195  chpchtsum  27200  dchrelbas2  27218  bposlem7  27271  lgsneg  27302  lgsne0  27316  lgsprme0  27320  lgsqrlem2  27328  lgsquadlem1  27361  lgsquadlem2  27362  2lgs  27388  2lgsoddprm  27397  2sqreultb  27440  lrrecval2  27950  subscan1d  28113  n0lesm1lt  28377  bdaypw2bnd  28475  elreno2  28505  istrkg3ld  28547  tgcgr4  28617  iscgra1  28896  isleag  28933  iseqlg  28953  axcontlem7  29057  elntg2  29072  edg0iedg0  29142  ausgrusgrb  29252  usgr1v0edg  29344  nb3grprlem2  29468  uvtx01vtx  29484  cplgr3v  29522  vtxd0nedgb  29575  vtxdusgr0edgnelALT  29583  1egrvtxdg0  29598  upgr2wlk  29753  wlkp1lem8  29765  dfpth2  29815  wwlksnextbi  29980  s3wwlks2on  30042  sps3wwlks2on  30043  elwwlks2  30055  elwspths2spth  30056  rusgrnumwwlkl1  30057  clwwlkwwlksb  30142  0pth  30213  upgriseupth  30295  eupth2lem2  30307  eupth2lem3lem4  30319  eupth2lem3lem6  30321  nfrgr2v  30360  frgr3v  30363  fusgr2wsp2nb  30422  fusgreg2wsp  30424  extwwlkfab  30440  numclwwlk2lem1  30464  frgrreggt1  30481  imsmetlem  30779  ipz  30808  bnsscmcl  30957  minvecolem4  30969  hvsubcan  31163  hoeq2  31920  leoptri  32225  atcv0eq  32468  elimifd  32631  fdifsupp  32777  ressupprn  32782  gtiso  32793  2ndpreima  32800  fpwrelmapffslem  32824  quad3d  32841  xnn01gt  32862  fzsplit3  32885  fzo0opth  32895  islinds5  33450  grplsmid  33487  r1pid2OLD  33692  selvply1rhmlem2  33705  fldextrspunlsp  33858  constrsuc  33922  smatrcl  33980  rhmpreimacnlem  34068  pstmfval  34080  lmlim  34131  dya2ub  34454  eulerpartlemr  34558  isrrvv  34627  ballotlemsima  34700  signsvfn  34766  subfacp1lem3  35410  subfacp1lem5  35412  erdszelem1  35419  erdsze  35430  erdsze2lem2  35432  satf0op  35605  fmlafvel  35613  isfmlasuc  35616  filnetlem4  36609  bj-issetwt  37228  bj-sbceqgALT  37255  bj-raldifsn  37458  bj-idreseq  37522  bj-elid6  37530  bj-imdirval3  37544  bj-imdirco  37550  poimirlem24  38011  itg2addnclem2  38039  ftc1anclem1  38060  areacirclem1  38075  areacirclem5  38079  metf1o  38122  isass  38213  rngosn3  38291  brxrn  38750  lsatcv0eq  39539  cmtbr2N  39745  atlatmstc  39811  1cvrco  39964  cdleme3  40729  cdleme7  40741  cdlemg10c  41131  dvhopellsm  41609  dibord  41651  dib1dim2  41660  diblsmopel  41663  dihopelvalcpre  41740  dih1dimatlem  41821  hdmap14lem13  42372  hdmapoc  42423  cxp112d  42818  cxp111d  42819  elrfirn  43144  jm2.19lem2  43435  pwfi2f1o  43541  proot1ex  43641  isoeq145d  43863  sqrtcval  44085  brfvidRP  44132  uneqsn  44469  ntrclsfveq  44506  ntrclskb  44513  ntrclsk3  44514  ntrneiel2  44530  k0004lem3  44593  bcc0  44784  pwpwuni  45505  disjinfi  45639  rnmptbd2  45693  rnmptbd  45700  infxrbnd2  45813  ltmulneg  45836  ltdiv23neg  45838  rexabsle  45862  uzub  45874  supxrleubrnmptf  45894  supminfxr  45907  limsupre2lem  46167  limsupre2mpt  46173  limsupre3mpt  46177  limsupreuz  46180  limsuplt2  46196  liminflimsupclim  46250  xlimpnfxnegmnf  46257  liminfpnfuz  46259  xlimclim  46267  xlimbr  46270  xlimclim2lem  46282  xlimmnfmpt  46286  xlimpnfmpt  46287  fourierdlem113  46662  isvonmbl  47081  chnsubseqwl  47324  reuf1odnf  47570  addsubeq0  47759  ltnltne  47762  ceilbi  47800  iccpartgtl  47901  iccpartleu  47903  iccpartgel  47904  reuprpr  47998  fmtnoprmfac1  48043  fmtnoprmfac2  48045  quad1  48111  requad1  48113  requad2  48114  bits0ALTV  48170  bgoldbtbndlem1  48296  clnbgrel  48319  clnbupgrel  48325  dfsclnbgr6  48349  isubgredg  48357  gpgiedgdmel  48540  opgpgvtx  48546  gpg3kgrtriexlem5  48578  0nodd  48661  2nodd  48663  rngcinvALTV  48767  ringcinvALTV  48801  islindeps  48944  snlindsntor  48962  blen1b  49079  nn0sumshdiglem1  49112  0aryfvalel  49125  rrx2plordisom  49214  ehl2eudis0lt  49217  eenglngeehlnmlem2  49229  rrx2linest  49233  line2  49243  line2x  49245  line2y  49246  itschlc0xyqsol1  49257  itsclquadeu  49268  map0cor  49345  joindm2  49458  meetdm2  49460  islmd  50155  iscmd  50156