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

Theorem 3bitrd 293
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 267 . 2 (𝜑 → (𝜓𝜃))
4 3bitrd.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitrd 267 1 (𝜑 → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  sbceqal  3454  elimhyp3v  4098  elimhyp4v  4099  keephyp3v  4104  frsn  5112  elpredg  5611  f1eq123d  6044  foeq123d  6045  f1oeq123d  6046  fnmptfvd  6228  ofrfval  6803  eloprabi  7121  fnmpt2ovd  7139  suppsnop  7196  smoeq  7334  infglbb  8280  wemapwe  8477  fseqenlem1  8730  dfac12lem2  8849  fin23lem22  9032  pwfseqlem5  9364  pwfseq  9365  enqbreq2  9621  lterpq  9671  ltdiv23  10793  lediv23  10794  negfi  10850  halfpos  11139  addltmul  11145  div4p1lem1div2  11164  supminf  11651  supxrbnd1  12023  supxrbnd2  12024  iccf1o  12187  fzshftral  12297  fzoshftral  12447  2tnp1ge0ge0  12492  dfceil2  12502  modirr  12603  hashen1  13021  seqcoll  13105  hash2prb  13111  s111  13248  swrdeq  13296  wrd2ind  13329  2swrd2eqwrdeq  13544  eqwrds3  13552  limsupgle  14056  tanaddlem  14735  dvdssub  14864  addmodlteqALT  14885  dvdsmod  14888  oddp1even  14906  nn0o1gt2  14935  nn0oddm1d2  14939  bitscmp  14998  saddisjlem  15024  smueqlem  15050  ncoprmgcdne1b  15201  cncongr1  15219  cncongr2  15220  prmreclem5  15462  4sqlem11  15497  4sqlem17  15503  vdwmc2  15521  ismre  16073  acsfn  16143  dfiso2  16255  brcic  16281  isssc  16303  setcinv  16563  intopsn  17076  sgrp1  17116  sgrp2nmndlem4  17238  nmzsubg  17458  conjnmzb  17518  gsmsymgreqlem2  17674  symgfixels  17677  f1omvdconj  17689  oddvdsnn0  17786  oddvds  17789  odcong  17791  odf1  17802  dpjeq  18281  pgpfac1lem2  18297  ring1  18425  lsmspsn  18905  lbsacsbs  18977  lpigen  19077  prmirredlem  19660  znf1o  19719  znleval  19722  znunit  19731  islinds2  19971  islindf4  19996  scmatf1  20156  isclo  20701  maxlp  20761  1stccn  21076  xkoinjcn  21300  elmptrab  21440  fbunfip  21483  elfm  21561  fmid  21574  flfnei  21605  isflf  21607  isfcls  21623  fclsopn  21628  isfcf  21648  cnextfun  21678  eltsms  21746  prdsxmetlem  21983  elmopn  22057  metss  22123  comet  22128  elbl4  22178  metuel2  22180  nrmmetd  22189  metdsge  22460  tchcph  22844  fmcfil  22878  rrxmet  22999  minveclem4  23011  shft2rab  23083  sca2rab  23087  volsup2  23179  mbfsup  23237  i1fmullem  23267  mbfi1fseqlem4  23291  xrge0f  23304  itg2monolem1  23323  ellimc2  23447  cnlimc  23458  mdegleb  23628  facth1  23728  ulm2  23943  sineq0  24077  coseq1  24078  efeq1  24079  sinord  24084  root1eq1  24296  angrtmuld  24338  quad2  24366  dcubic  24373  cubic2  24375  dquartlem1  24378  dquart  24380  quart  24388  rlimcnp  24492  lgamucov  24564  mumullem2  24706  chtub  24737  fsumvma  24738  fsumvma2  24739  chpchtsum  24744  bposlem7  24815  lgsneg  24846  lgsne0  24860  lgsprme0  24864  lgsqrlem2  24872  lgsquadlem1  24905  lgsquadlem2  24906  2lgs  24932  2lgsoddprm  24941  istrkg3ld  25160  tgcgr4  25226  iscgra1  25502  isleag  25533  iseqlg  25547  axcontlem7  25650  edg0iedg0  25800  isuslgra  25872  isusgra  25873  ausisusgra  25884  nbgraopALT  25953  nb3graprlem2  25981  cusgra3v  25993  sizeusglecusg  26014  uvtx01vtx  26020  is2wlk  26095  0pth  26100  wlkdvspthlem  26137  2wlkeq  26235  wwlknextbi  26253  clwwlkn2  26303  el2wlkonotot0  26399  el2wlkonotot  26400  el2wlksoton  26405  el2spthsoton  26406  el2wlksot  26407  el2pthsot  26408  isrusgusrgcl  26460  rusgrasn  26472  rusgranumwlkl1  26474  rusgra0edg  26482  eupath2lem2  26505  eupath2lem3  26506  frgra2v  26526  frgra3v  26529  usg2spot2nb  26592  numclwwlkovfel2  26610  numclwwlk2lem1  26629  numclwlk2lem2f1o  26632  frgrareggt1  26643  imsmetlem  26929  ipz  26958  bnsscmcl  27108  minvecolem4  27120  hvsubcan  27315  hoeq2  28074  leoptri  28379  atcv0eq  28622  elimifd  28746  gtiso  28861  2ndpreima  28868  fpwrelmapffslem  28895  fzsplit3  28940  isomnd  29032  ogrpinvlt  29055  smatrcl  29190  pstmfval  29267  lmlim  29321  dya2ub  29659  eulerpartlemr  29763  isrrvv  29832  ballotlemsima  29904  signsvfn  29985  subfacp1lem3  30418  subfacp1lem5  30420  erdszelem1  30427  erdsze  30438  erdsze2lem2  30440  filnetlem4  31546  bj-issetwt  32053  bj-sbceqgALT  32089  csbwrecsg  32349  poimirlem24  32603  itg2addnclem2  32632  ftc1anclem1  32655  areacirclem1  32670  areacirclem5  32674  metf1o  32721  isass  32815  rngosn3  32893  lsatcv0eq  33352  cmtbr2N  33558  atlatmstc  33624  1cvrco  33776  cdleme3  34542  cdleme7  34554  cdlemg10c  34945  dvhopellsm  35424  dibord  35466  dib1dim2  35475  diblsmopel  35478  dihopelvalcpre  35555  dih1dimatlem  35636  hdmap14lem13  36190  hdmapoc  36241  elrfirn  36276  jm2.19lem2  36575  pwfi2f1o  36684  proot1ex  36798  brfvidRP  36999  uneqsn  37341  ntrclsfveq  37380  ntrclskb  37387  ntrclsk3  37388  ntrneiel2  37404  k0004lem3  37467  bcc0  37561  pwpwuni  38250  rnmptpr  38353  disjinfi  38375  mapsnend  38386  infxrbnd2  38526  ltmulneg  38556  ltdiv23neg  38558  fourierdlem113  39112  isvonmbl  39528  2reu4a  39838  iccpartgtl  39964  iccpartleu  39966  iccpartgel  39967  fmtnoprmfac1  40015  fmtnoprmfac2  40017  bits0ALTV  40128  bgoldbtbndlem1  40221  pfxeq  40267  ltnltne  40345  ausgrusgrb  40395  nb3grprlem2  40609  uvtxa01vtx0  40623  cplgr3v  40657  vtxd0nedgb  40703  vtxdusgr0edgnelALT  40711  1egrvtxdg0  40727  1wlkeq  40838  upgr2wlk  40876  1wlkp1lem8  40889  wwlksnextbi  41100  wspthsnwspthsnon  41122  s3wwlks2on  41160  elwwlks2  41170  elwspths2spth  41171  rusgrnumwwlkl1  41172  0pth-av  41293  upgriseupth  41375  eupth2lem2  41387  eupth2lem3lem4  41399  eupth2lem3lem6  41401  nfrgr2v  41442  frgr3v  41445  fusgr2wsp2nb  41498  fusgreg2wsp  41500  av-extwwlkfab  41520  av-numclwwlk2lem1  41532  av-frgrareggt1  41547  0nodd  41600  2nodd  41602  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848  islindeps  42036  snlindsntor  42054  blen1b  42180  nn0sumshdiglem1  42213
  Copyright terms: Public domain W3C validator