Theorem 3bitrd 305

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 279	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitrd.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 279	1 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  2reu4lem  4497  elimhyp3v  4568  elimhyp4v  4569  keephyp3v  4574  ralsng  4651  opeqsng  5478  snopeqop  5481  frsn  5742  f1eq123d  6809  foeq123d  6810  f1oeq123d  6811  fnmptfvd  7030  fnotovb  7455  ofrfvalg  7677  eloprabi  8060  fnmpoovd  8084  suppsnop  8175  smoeq  8362  naddasslem1  8704  naddasslem2  8705  mapsnend  9048  infglbb  9502  wemapwe  9709  fseqenlem1  10036  dfac12lem2  10157  fin23lem22  10339  pwfseqlem5  10675  pwfseq  10676  enqbreq2  10932  lterpq  10982  ltdiv23  12131  lediv23  12132  negfi  12189  halfpos  12469  addltmul  12475  div4p1lem1div2  12494  supminf  12949  supxrbnd1  13335  supxrbnd2  13336  iccf1o  13511  fzshftral  13630  fzoshftral  13798  2tnp1ge0ge0  13844  dfceil2  13854  modirr  13958  hashen1  14386  seqcoll  14480  hash2prb  14488  hashle2prv  14494  hash3tpb  14511  s111  14631  swrdspsleq  14681  pfxnd0  14704  pfxeq  14712  wrd2ind  14739  2swrd2eqwrdeq  14970  eqwrds3  14978  limsupgle  15491  tanaddlem  16182  dvdssub  16321  addmodlteqALT  16342  dvdsmod  16346  oddp1even  16361  nn0o1gt2  16398  nn0oddm1d2  16402  bitscmp  16455  saddisjlem  16481  smueqlem  16507  ncoprmgcdne1b  16667  cncongr1  16684  cncongr2  16685  prmreclem5  16938  4sqlem11  16973  4sqlem17  16979  vdwmc2  16997  ismre  17600  acsfn  17669  dfiso2  17783  brcic  17809  isssc  17831  setcinv  18101  cat1  18108  intopsn  18630  sgrp1  18705  sgrppropd  18707  sgrp2nmndlem4  18904  nmzsubg  19146  eqg0subg  19177  conjnmzb  19234  gsmsymgreqlem2  19410  symgfixels  19413  f1omvdconj  19425  oddvdsnn0  19523  oddvds  19526  odcong  19528  odf1  19541  dpjeq  20040  pgpfac1lem2  20056  ring1  20268  rngcinv  20595  ringcinv  20629  lsmspsn  21040  lbsacsbs  21115  rngqiprngimf1lem  21253  lpigen  21294  prmirredlem  21431  znf1o  21510  znleval  21513  znunit  21522  islinds2  21771  islindf4  21796  psdmul  22102  scmatf1  22467  isclo  23023  maxlp  23083  1stccn  23399  xkoinjcn  23623  elmptrab  23763  fbunfip  23805  elfm  23883  fmid  23896  flfnei  23927  isflf  23929  isfcls  23945  fclsopn  23950  isfcf  23970  cnextfun  24000  eltsms  24069  prdsxmetlem  24305  elmopn  24379  metss  24445  comet  24450  elbl4  24500  metuel2  24502  nrmmetd  24511  metdsge  24787  tcphcph  25187  fmcfil  25222  cmscsscms  25323  rrxmet  25358  minveclem4  25382  shft2rab  25459  sca2rab  25463  volsup2  25556  mbfsup  25615  i1fmullem  25645  mbfi1fseqlem4  25669  xrge0f  25682  itg2monolem1  25701  ellimc2  25828  cnlimc  25839  mdegleb  26019  r1pid2  26117  facth1  26122  ulm2  26344  sineq0  26483  coseq1  26484  efeq1  26487  sinord  26493  root1eq1  26715  angrtmuld  26768  affineequiv3  26785  quad2  26799  dcubic  26806  cubic2  26808  dquartlem1  26811  dquart  26813  quart  26821  rlimcnp  26925  lgamucov  26998  mumullem2  27140  chtub  27173  fsumvma  27174  fsumvma2  27175  chpchtsum  27180  dchrelbas2  27198  bposlem7  27251  lgsneg  27282  lgsne0  27296  lgsprme0  27300  lgsqrlem2  27308  lgsquadlem1  27341  lgsquadlem2  27342  2lgs  27368  2lgsoddprm  27377  2sqreultb  27420  lrrecval2  27890  istrkg3ld  28386  tgcgr4  28456  iscgra1  28735  isleag  28772  iseqlg  28792  axcontlem7  28895  elntg2  28910  edg0iedg0  28980  ausgrusgrb  29090  usgr1v0edg  29182  nb3grprlem2  29306  uvtx01vtx  29322  cplgr3v  29360  vtxd0nedgb  29414  vtxdusgr0edgnelALT  29422  1egrvtxdg0  29437  upgr2wlk  29594  wlkp1lem8  29606  dfpth2  29657  wwlksnextbi  29822  s3wwlks2on  29884  elwwlks2  29894  elwspths2spth  29895  rusgrnumwwlkl1  29896  clwwlkwwlksb  29981  0pth  30052  upgriseupth  30134  eupth2lem2  30146  eupth2lem3lem4  30158  eupth2lem3lem6  30160  nfrgr2v  30199  frgr3v  30202  fusgr2wsp2nb  30261  fusgreg2wsp  30263  extwwlkfab  30279  numclwwlk2lem1  30303  frgrreggt1  30320  imsmetlem  30617  ipz  30646  bnsscmcl  30795  minvecolem4  30807  hvsubcan  31001  hoeq2  31758  leoptri  32063  atcv0eq  32306  elimifd  32470  fdifsupp  32608  ressupprn  32613  gtiso  32624  2ndpreima  32631  fpwrelmapffslem  32655  quad3d  32673  xnn01gt  32693  fzsplit3  32716  fzo0opth  32728  isomnd  33015  ogrpinvlt  33037  islinds5  33328  grplsmid  33365  r1pid2OLD  33564  fldextrspunlsp  33661  constrsuc  33718  smatrcl  33773  rhmpreimacnlem  33861  pstmfval  33873  lmlim  33924  dya2ub  34248  eulerpartlemr  34352  isrrvv  34421  ballotlemsima  34494  signsvfn  34560  subfacp1lem3  35150  subfacp1lem5  35152  erdszelem1  35159  erdsze  35170  erdsze2lem2  35172  satf0op  35345  fmlafvel  35353  isfmlasuc  35356  filnetlem4  36345  bj-issetwt  36839  bj-sbceqgALT  36866  bj-raldifsn  37064  bj-idreseq  37126  bj-elid6  37134  bj-imdirval3  37148  bj-imdirco  37154  poimirlem24  37614  itg2addnclem2  37642  ftc1anclem1  37663  areacirclem1  37678  areacirclem5  37682  metf1o  37725  isass  37816  rngosn3  37894  brxrn  38338  lsatcv0eq  39011  cmtbr2N  39217  atlatmstc  39283  1cvrco  39437  cdleme3  40202  cdleme7  40214  cdlemg10c  40604  dvhopellsm  41082  dibord  41124  dib1dim2  41133  diblsmopel  41136  dihopelvalcpre  41213  dih1dimatlem  41294  hdmap14lem13  41845  hdmapoc  41896  cxp112d  42337  cxp111d  42338  elrfirn  42665  jm2.19lem2  42961  pwfi2f1o  43067  proot1ex  43167  isoeq145d  43390  sqrtcval  43612  brfvidRP  43659  uneqsn  43996  ntrclsfveq  44033  ntrclskb  44040  ntrclsk3  44041  ntrneiel2  44057  k0004lem3  44120  bcc0  44312  pwpwuni  45029  disjinfi  45164  rnmptbd2  45221  rnmptbd  45228  infxrbnd2  45344  ltmulneg  45367  ltdiv23neg  45369  rexabsle  45394  uzub  45406  supxrleubrnmptf  45426  supminfxr  45439  limsupre2lem  45701  limsupre2mpt  45707  limsupre3mpt  45711  limsupreuz  45714  limsuplt2  45730  liminflimsupclim  45784  xlimpnfxnegmnf  45791  liminfpnfuz  45793  xlimclim  45801  xlimbr  45804  xlimclim2lem  45816  xlimmnfmpt  45820  xlimpnfmpt  45821  fourierdlem113  46196  isvonmbl  46615  reuf1odnf  47084  addsubeq0  47273  ltnltne  47276  ceilbi  47310  iccpartgtl  47388  iccpartleu  47390  iccpartgel  47391  reuprpr  47485  fmtnoprmfac1  47527  fmtnoprmfac2  47529  quad1  47582  requad1  47584  requad2  47585  bits0ALTV  47641  bgoldbtbndlem1  47767  clnbgrel  47790  clnbupgrel  47796  dfsclnbgr6  47819  isubgredg  47827  gpgiedgdmel  48001  opgpgvtx  48007  gpg3kgrtriexlem5  48037  0nodd  48093  2nodd  48095  rngcinvALTV  48199  ringcinvALTV  48233  islindeps  48377  snlindsntor  48395  blen1b  48516  nn0sumshdiglem1  48549  0aryfvalel  48562  rrx2plordisom  48651  ehl2eudis0lt  48654  eenglngeehlnmlem2  48666  rrx2linest  48670  line2  48680  line2x  48682  line2y  48683  itschlc0xyqsol1  48694  itsclquadeu  48705  map0cor  48781  joindm2  48890  meetdm2  48892  islmd  49483  iscmd  49484