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

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
StepHypRef Expression
1 3bitrd.1 . . 3 (𝜑 → (𝜓𝜒))
2 3bitrd.2 . . 3 (𝜑 → (𝜒𝜃))
31, 2bitrd 280 . 2 (𝜑 → (𝜓𝜃))
4 3bitrd.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitrd 280 1 (𝜑 → (𝜓𝜏))
Colors of variables: wff setvar class
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:  sbceqal  3834  2reu4lem  4463  elimhyp3v  4530  elimhyp4v  4531  keephyp3v  4536  opeqsng  5385  snopeqop  5388  frsn  5633  elpredg  6156  f1eq123d  6602  foeq123d  6603  f1oeq123d  6604  fnmptfvd  6804  fnotovb  7195  ofrfval  7406  eloprabi  7752  fnmpoovd  7773  suppsnop  7835  smoeq  7978  mapsnend  8577  infglbb  8944  wemapwe  9149  fseqenlem1  9439  dfac12lem2  9559  fin23lem22  9738  pwfseqlem5  10074  pwfseq  10075  enqbreq2  10331  lterpq  10381  ltdiv23  11520  lediv23  11521  negfi  11578  halfpos  11856  addltmul  11862  div4p1lem1div2  11881  supminf  12324  supxrbnd1  12704  supxrbnd2  12705  iccf1o  12872  fzshftral  12985  fzoshftral  13144  2tnp1ge0ge0  13189  dfceil2  13199  modirr  13300  hashen1  13721  seqcoll  13812  hash2prb  13820  hashle2prv  13826  s111  13959  swrdspsleq  14017  pfxnd0  14040  pfxeq  14048  wrd2ind  14075  2swrd2eqwrdeq  14305  eqwrds3  14315  limsupgle  14824  tanaddlem  15509  dvdssub  15644  addmodlteqALT  15665  dvdsmod  15668  oddp1even  15683  nn0o1gt2  15722  nn0oddm1d2  15726  bitscmp  15777  saddisjlem  15803  smueqlem  15829  ncoprmgcdne1b  15984  cncongr1  16001  cncongr2  16002  prmreclem5  16246  4sqlem11  16281  4sqlem17  16287  vdwmc2  16305  ismre  16851  acsfn  16920  dfiso2  17032  brcic  17058  isssc  17080  setcinv  17340  intopsn  17854  sgrp1  17900  sgrp2nmndlem4  18033  nmzsubg  18257  conjnmzb  18333  gsmsymgreqlem2  18490  symgfixels  18493  f1omvdconj  18505  oddvdsnn0  18603  oddvds  18606  odcong  18608  odf1  18620  dpjeq  19112  pgpfac1lem2  19128  ring1  19283  lsmspsn  19787  lbsacsbs  19859  lpigen  19959  prmirredlem  20570  znf1o  20628  znleval  20631  znunit  20640  islinds2  20887  islindf4  20912  scmatf1  21070  isclo  21625  maxlp  21685  1stccn  22001  xkoinjcn  22225  elmptrab  22365  fbunfip  22407  elfm  22485  fmid  22498  flfnei  22529  isflf  22531  isfcls  22547  fclsopn  22552  isfcf  22572  cnextfun  22602  eltsms  22670  prdsxmetlem  22907  elmopn  22981  metss  23047  comet  23052  elbl4  23102  metuel2  23104  nrmmetd  23113  metdsge  23386  tcphcph  23769  fmcfil  23804  cmscsscms  23905  rrxmet  23940  minveclem4  23964  shft2rab  24038  sca2rab  24042  volsup2  24135  mbfsup  24194  i1fmullem  24224  mbfi1fseqlem4  24248  xrge0f  24261  itg2monolem1  24280  ellimc2  24404  cnlimc  24415  mdegleb  24587  facth1  24687  ulm2  24902  sineq0  25038  coseq1  25039  efeq1  25040  sinord  25045  root1eq1  25263  angrtmuld  25313  affineequiv3  25330  quad2  25344  dcubic  25351  cubic2  25353  dquartlem1  25356  dquart  25358  quart  25366  rlimcnp  25471  lgamucov  25543  mumullem2  25685  chtub  25716  fsumvma  25717  fsumvma2  25718  chpchtsum  25723  dchrelbas2  25741  bposlem7  25794  lgsneg  25825  lgsne0  25839  lgsprme0  25843  lgsqrlem2  25851  lgsquadlem1  25884  lgsquadlem2  25885  2lgs  25911  2lgsoddprm  25920  2sqreultb  25963  istrkg3ld  26175  tgcgr4  26245  iscgra1  26524  isleag  26561  iseqlg  26581  axcontlem7  26684  elntg2  26699  edg0iedg0  26768  ausgrusgrb  26878  usgr1v0edg  26967  nb3grprlem2  27091  uvtx01vtx  27107  cplgr3v  27145  vtxd0nedgb  27198  vtxdusgr0edgnelALT  27206  1egrvtxdg0  27221  upgr2wlk  27378  wlkp1lem8  27390  wwlksnextbi  27600  s3wwlks2on  27663  elwwlks2  27673  elwspths2spth  27674  rusgrnumwwlkl1  27675  clwwlkwwlksb  27761  0pth  27832  upgriseupth  27914  eupth2lem2  27926  eupth2lem3lem4  27938  eupth2lem3lem6  27940  nfrgr2v  27979  frgr3v  27982  fusgr2wsp2nb  28041  fusgreg2wsp  28043  extwwlkfab  28059  numclwwlk2lem1  28083  frgrreggt1  28100  imsmetlem  28395  ipz  28424  bnsscmcl  28573  minvecolem4  28585  hvsubcan  28779  hoeq2  29536  leoptri  29841  atcv0eq  30084  elimifd  30226  gtiso  30363  2ndpreima  30370  fpwrelmapffslem  30395  xnn01gt  30422  fzsplit3  30444  isomnd  30630  ogrpinvlt  30652  islinds5  30860  smatrcl  30961  pstmfval  31036  lmlim  31090  dya2ub  31428  eulerpartlemr  31532  isrrvv  31601  ballotlemsima  31673  signsvfn  31752  subfacp1lem3  32327  subfacp1lem5  32329  erdszelem1  32336  erdsze  32347  erdsze2lem2  32349  satf0op  32522  fmlafvel  32530  isfmlasuc  32533  filnetlem4  33627  bj-issetwt  34087  bj-sbceqgALT  34117  bj-raldifsn  34287  bj-idreseq  34347  bj-elid6  34355  bj-imdirval3  34367  csbwrecsg  34491  poimirlem24  34798  itg2addnclem2  34826  ftc1anclem1  34849  areacirclem1  34864  areacirclem5  34868  metf1o  34913  isass  35007  rngosn3  35085  brxrn  35508  lsatcv0eq  36065  cmtbr2N  36271  atlatmstc  36337  1cvrco  36490  cdleme3  37255  cdleme7  37267  cdlemg10c  37657  dvhopellsm  38135  dibord  38177  dib1dim2  38186  diblsmopel  38189  dihopelvalcpre  38266  dih1dimatlem  38347  hdmap14lem13  38898  hdmapoc  38949  elrfirn  39172  jm2.19lem2  39467  pwfi2f1o  39576  proot1ex  39681  brfvidRP  39913  uneqsn  40253  ntrclsfveq  40292  ntrclskb  40299  ntrclsk3  40300  ntrneiel2  40316  k0004lem3  40379  bcc0  40552  pwpwuni  41199  disjinfi  41334  rnmptbd2  41401  rnmptbd  41408  infxrbnd2  41517  ltmulneg  41544  ltdiv23neg  41546  rexabsle  41573  uzub  41585  supxrleubrnmptf  41607  supminfxr  41620  limsupre2lem  41885  limsupre2mpt  41891  limsupre3mpt  41895  limsupreuz  41898  limsuplt2  41914  liminflimsupclim  41968  xlimpnfxnegmnf  41975  liminfpnfuz  41977  xlimclim  41985  xlimbr  41988  xlimclim2lem  42000  xlimmnfmpt  42004  xlimpnfmpt  42005  fourierdlem113  42385  isvonmbl  42801  reuf1odnf  43187  addsubeq0  43377  ltnltne  43380  iccpartgtl  43433  iccpartleu  43435  iccpartgel  43436  reuprpr  43532  fmtnoprmfac1  43574  fmtnoprmfac2  43576  quad1  43632  requad1  43634  requad2  43635  bits0ALTV  43691  bgoldbtbndlem1  43817  0nodd  43924  2nodd  43926  rngcinv  44150  rngcinvALTV  44162  ringcinv  44201  ringcinvALTV  44225  islindeps  44406  snlindsntor  44424  blen1b  44546  nn0sumshdiglem1  44579  rrx2plordisom  44608  ehl2eudis0lt  44611  eenglngeehlnmlem2  44623  rrx2linest  44627  line2  44637  line2x  44639  line2y  44640  itschlc0xyqsol1  44651  itsclquadeu  44662
  Copyright terms: Public domain W3C validator