MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitrd Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 3bitrd.1 . . 3 (𝜑 → (𝜓𝜒))
2 3bitrd.2 . . 3 (𝜑 → (𝜒𝜃))
31, 2bitrd 279 . 2 (𝜑 → (𝜓𝜃))
4 3bitrd.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitrd 279 1 (𝜑 → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  sbceqalOLD  3807  2reu4lem  4484  elimhyp3v  4554  elimhyp4v  4555  keephyp3v  4560  ralsng  4635  opeqsng  5461  snopeqop  5464  frsn  5720  f1eq123d  6777  foeq123d  6778  f1oeq123d  6779  fnmptfvd  6992  fnotovb  7408  ofrfvalg  7626  eloprabi  7996  fnmpoovd  8020  suppsnop  8110  smoeq  8297  naddasslem1  8639  naddasslem2  8640  mapsnend  8981  infglbb  9428  wemapwe  9634  fseqenlem1  9961  dfac12lem2  10081  fin23lem22  10264  pwfseqlem5  10600  pwfseq  10601  enqbreq2  10857  lterpq  10907  ltdiv23  12047  lediv23  12048  negfi  12105  halfpos  12384  addltmul  12390  div4p1lem1div2  12409  supminf  12861  supxrbnd1  13241  supxrbnd2  13242  iccf1o  13414  fzshftral  13530  fzoshftral  13690  2tnp1ge0ge0  13735  dfceil2  13745  modirr  13848  hashen1  14271  seqcoll  14364  hash2prb  14372  hashle2prv  14378  s111  14504  swrdspsleq  14554  pfxnd0  14577  pfxeq  14585  wrd2ind  14612  2swrd2eqwrdeq  14843  eqwrds3  14851  limsupgle  15360  tanaddlem  16049  dvdssub  16187  addmodlteqALT  16208  dvdsmod  16212  oddp1even  16227  nn0o1gt2  16264  nn0oddm1d2  16268  bitscmp  16319  saddisjlem  16345  smueqlem  16371  ncoprmgcdne1b  16527  cncongr1  16544  cncongr2  16545  prmreclem5  16793  4sqlem11  16828  4sqlem17  16834  vdwmc2  16852  ismre  17471  acsfn  17540  dfiso2  17656  brcic  17682  isssc  17704  setcinv  17977  cat1  17984  intopsn  18510  sgrp1  18556  sgrp2nmndlem4  18739  nmzsubg  18968  conjnmzb  19044  gsmsymgreqlem2  19214  symgfixels  19217  f1omvdconj  19229  oddvdsnn0  19327  oddvds  19330  odcong  19332  odf1  19345  dpjeq  19839  pgpfac1lem2  19855  ring1  20027  lsmspsn  20548  lbsacsbs  20620  lpigen  20729  prmirredlem  20896  znf1o  20961  znleval  20964  znunit  20973  islinds2  21222  islindf4  21247  scmatf1  21883  isclo  22441  maxlp  22501  1stccn  22817  xkoinjcn  23041  elmptrab  23181  fbunfip  23223  elfm  23301  fmid  23314  flfnei  23345  isflf  23347  isfcls  23363  fclsopn  23368  isfcf  23388  cnextfun  23418  eltsms  23487  prdsxmetlem  23724  elmopn  23798  metss  23867  comet  23872  elbl4  23922  metuel2  23924  nrmmetd  23933  metdsge  24215  tcphcph  24604  fmcfil  24639  cmscsscms  24740  rrxmet  24775  minveclem4  24799  shft2rab  24875  sca2rab  24879  volsup2  24972  mbfsup  25031  i1fmullem  25061  mbfi1fseqlem4  25086  xrge0f  25099  itg2monolem1  25118  ellimc2  25244  cnlimc  25255  mdegleb  25432  facth1  25532  ulm2  25747  sineq0  25883  coseq1  25884  efeq1  25887  sinord  25893  root1eq1  26111  angrtmuld  26161  affineequiv3  26178  quad2  26192  dcubic  26199  cubic2  26201  dquartlem1  26204  dquart  26206  quart  26214  rlimcnp  26318  lgamucov  26390  mumullem2  26532  chtub  26563  fsumvma  26564  fsumvma2  26565  chpchtsum  26570  dchrelbas2  26588  bposlem7  26641  lgsneg  26672  lgsne0  26686  lgsprme0  26690  lgsqrlem2  26698  lgsquadlem1  26731  lgsquadlem2  26732  2lgs  26758  2lgsoddprm  26767  2sqreultb  26810  lrrecval2  27255  istrkg3ld  27406  tgcgr4  27476  iscgra1  27755  isleag  27792  iseqlg  27812  axcontlem7  27922  elntg2  27937  edg0iedg0  28009  ausgrusgrb  28119  usgr1v0edg  28208  nb3grprlem2  28332  uvtx01vtx  28348  cplgr3v  28386  vtxd0nedgb  28439  vtxdusgr0edgnelALT  28447  1egrvtxdg0  28462  upgr2wlk  28619  wlkp1lem8  28631  wwlksnextbi  28842  s3wwlks2on  28904  elwwlks2  28914  elwspths2spth  28915  rusgrnumwwlkl1  28916  clwwlkwwlksb  29001  0pth  29072  upgriseupth  29154  eupth2lem2  29166  eupth2lem3lem4  29178  eupth2lem3lem6  29180  nfrgr2v  29219  frgr3v  29222  fusgr2wsp2nb  29281  fusgreg2wsp  29283  extwwlkfab  29299  numclwwlk2lem1  29323  frgrreggt1  29340  imsmetlem  29635  ipz  29664  bnsscmcl  29813  minvecolem4  29825  hvsubcan  30019  hoeq2  30776  leoptri  31081  atcv0eq  31324  elimifd  31468  ressupprn  31608  gtiso  31617  2ndpreima  31624  fpwrelmapffslem  31652  xnn01gt  31678  fzsplit3  31700  isomnd  31912  ogrpinvlt  31934  islinds5  32159  grplsmid  32188  smatrcl  32380  rhmpreimacnlem  32468  pstmfval  32480  lmlim  32531  dya2ub  32873  eulerpartlemr  32977  isrrvv  33046  ballotlemsima  33118  signsvfn  33197  subfacp1lem3  33779  subfacp1lem5  33781  erdszelem1  33788  erdsze  33799  erdsze2lem2  33801  satf0op  33974  fmlafvel  33982  isfmlasuc  33985  filnetlem4  34856  bj-issetwt  35344  bj-sbceqgALT  35372  bj-raldifsn  35574  bj-idreseq  35636  bj-elid6  35644  bj-imdirval3  35658  bj-imdirco  35664  poimirlem24  36105  itg2addnclem2  36133  ftc1anclem1  36154  areacirclem1  36169  areacirclem5  36173  metf1o  36217  isass  36308  rngosn3  36386  brxrn  36839  lsatcv0eq  37512  cmtbr2N  37718  atlatmstc  37784  1cvrco  37938  cdleme3  38703  cdleme7  38715  cdlemg10c  39105  dvhopellsm  39583  dibord  39625  dib1dim2  39634  diblsmopel  39637  dihopelvalcpre  39714  dih1dimatlem  39795  hdmap14lem13  40346  hdmapoc  40397  elrfirn  41021  jm2.19lem2  41317  pwfi2f1o  41426  proot1ex  41531  isoeq145d  41698  sqrtcval  41920  brfvidRP  41967  uneqsn  42304  ntrclsfveq  42341  ntrclskb  42348  ntrclsk3  42349  ntrneiel2  42365  k0004lem3  42428  bcc0  42627  pwpwuni  43272  disjinfi  43419  rnmptbd2  43484  rnmptbd  43491  infxrbnd2  43610  ltmulneg  43634  ltdiv23neg  43636  rexabsle  43661  uzub  43673  supxrleubrnmptf  43693  supminfxr  43706  limsupre2lem  43972  limsupre2mpt  43978  limsupre3mpt  43982  limsupreuz  43985  limsuplt2  44001  liminflimsupclim  44055  xlimpnfxnegmnf  44062  liminfpnfuz  44064  xlimclim  44072  xlimbr  44075  xlimclim2lem  44087  xlimmnfmpt  44091  xlimpnfmpt  44092  fourierdlem113  44467  isvonmbl  44886  reuf1odnf  45346  addsubeq0  45535  ltnltne  45538  iccpartgtl  45625  iccpartleu  45627  iccpartgel  45628  reuprpr  45722  fmtnoprmfac1  45764  fmtnoprmfac2  45766  quad1  45819  requad1  45821  requad2  45822  bits0ALTV  45878  bgoldbtbndlem1  46004  0nodd  46111  2nodd  46113  rngcinv  46286  rngcinvALTV  46298  ringcinv  46337  ringcinvALTV  46361  islindeps  46541  snlindsntor  46559  blen1b  46681  nn0sumshdiglem1  46714  0aryfvalel  46727  rrx2plordisom  46816  ehl2eudis0lt  46819  eenglngeehlnmlem2  46831  rrx2linest  46835  line2  46845  line2x  46847  line2y  46848  itschlc0xyqsol1  46859  itsclquadeu  46870  map0cor  46928  joindm2  47008  meetdm2  47010
  Copyright terms: Public domain W3C validator