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

Theorem 3bitrd 292
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 266 . 2 (𝜑 → (𝜓𝜃))
4 3bitrd.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitrd 266 1 (𝜑 → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  sbceqal  3453  elimhyp3v  4097  elimhyp4v  4098  keephyp3v  4103  frsn  5102  elpredg  5597  f1eq123d  6029  foeq123d  6030  f1oeq123d  6031  fnmptfvd  6213  ofrfval  6781  eloprabi  7099  fnmpt2ovd  7117  suppsnop  7174  smoeq  7312  infglbb  8258  wemapwe  8455  fseqenlem1  8708  dfac12lem2  8827  fin23lem22  9010  pwfseqlem5  9342  pwfseq  9343  enqbreq2  9599  lterpq  9649  ltdiv23  10766  lediv23  10767  negfi  10823  halfpos  11112  addltmul  11118  div4p1lem1div2  11137  supminf  11610  supxrbnd1  11982  supxrbnd2  11983  iccf1o  12146  fzshftral  12255  fzoshftral  12405  2tnp1ge0ge0  12450  dfceil2  12460  modirr  12561  hashen1  12976  seqcoll  13060  hash2prb  13066  s111  13197  swrdeq  13245  wrd2ind  13278  2swrd2eqwrdeq  13493  eqwrds3  13501  limsupgle  14005  tanaddlem  14684  dvdssub  14813  addmodlteqALT  14834  dvdsmod  14837  oddp1even  14855  nn0o1gt2  14884  nn0oddm1d2  14888  bitscmp  14947  saddisjlem  14973  smueqlem  14999  ncoprmgcdne1b  15150  cncongr1  15168  cncongr2  15169  prmreclem5  15411  4sqlem11  15446  4sqlem17  15452  vdwmc2  15470  ismre  16022  acsfn  16092  dfiso2  16204  brcic  16230  isssc  16252  setcinv  16512  intopsn  17025  sgrp1  17065  sgrp2nmndlem4  17187  nmzsubg  17407  conjnmzb  17467  gsmsymgreqlem2  17623  symgfixels  17626  f1omvdconj  17638  oddvdsnn0  17735  oddvds  17738  odcong  17740  odf1  17751  dpjeq  18230  pgpfac1lem2  18246  ring1  18374  lsmspsn  18854  lbsacsbs  18926  lpigen  19026  prmirredlem  19608  znf1o  19667  znleval  19670  znunit  19679  islinds2  19919  islindf4  19944  scmatf1  20104  isclo  20649  maxlp  20709  1stccn  21024  xkoinjcn  21248  elmptrab  21388  fbunfip  21431  elfm  21509  fmid  21522  flfnei  21553  isflf  21555  isfcls  21571  fclsopn  21576  isfcf  21596  cnextfun  21626  eltsms  21694  prdsxmetlem  21931  elmopn  22005  metss  22071  comet  22076  elbl4  22126  metuel2  22128  nrmmetd  22137  metdsge  22408  tchcph  22789  fmcfil  22823  rrxmet  22944  minveclem4  22956  shft2rab  23028  sca2rab  23032  volsup2  23124  mbfsup  23182  i1fmullem  23212  mbfi1fseqlem4  23236  xrge0f  23249  itg2monolem1  23268  ellimc2  23392  cnlimc  23403  mdegleb  23573  facth1  23673  ulm2  23888  sineq0  24022  coseq1  24023  efeq1  24024  sinord  24029  root1eq1  24241  angrtmuld  24283  quad2  24311  dcubic  24318  cubic2  24320  dquartlem1  24323  dquart  24325  quart  24333  rlimcnp  24437  lgamucov  24509  mumullem2  24651  chtub  24682  fsumvma  24683  fsumvma2  24684  chpchtsum  24689  bposlem7  24760  lgsneg  24791  lgsne0  24805  lgsprme0  24809  lgsqrlem2  24817  lgsquadlem1  24850  lgsquadlem2  24851  2lgs  24877  2lgsoddprm  24886  istrkg3ld  25105  tgcgr4  25172  iscgra1  25448  isleag  25479  iseqlg  25493  axcontlem7  25596  isuslgra  25666  isusgra  25667  ausisusgra  25678  nbgraopALT  25747  nb3graprlem2  25775  cusgra3v  25787  sizeusglecusg  25808  uvtx01vtx  25814  is2wlk  25889  0pth  25894  wlkdvspthlem  25931  2wlkeq  26029  wwlknextbi  26047  clwwlkn2  26097  el2wlkonotot0  26193  el2wlkonotot  26194  el2wlksoton  26199  el2spthsoton  26200  el2wlksot  26201  el2pthsot  26202  isrusgusrgcl  26254  rusgrasn  26266  rusgranumwlkl1  26268  rusgra0edg  26276  eupath2lem2  26299  eupath2lem3  26300  frgra2v  26320  frgra3v  26323  usg2spot2nb  26386  numclwwlkovfel2  26404  numclwwlk2lem1  26423  numclwlk2lem2f1o  26426  frgrareggt1  26437  imsmetlem  26754  ipz  26790  bnsscmcl  26942  minvecolem4  26954  hvsubcan  27149  hoeq2  27908  leoptri  28213  atcv0eq  28456  elimifd  28580  gtiso  28695  2ndpreima  28702  fpwrelmapffslem  28729  fzsplit3  28774  isomnd  28866  ogrpinvlt  28889  smatrcl  29024  pstmfval  29101  lmlim  29155  dya2ub  29493  eulerpartlemr  29597  isrrvv  29666  ballotlemsima  29738  signsvfn  29819  subfacp1lem3  30252  subfacp1lem5  30254  erdszelem1  30261  erdsze  30272  erdsze2lem2  30274  filnetlem4  31380  bj-issetwt  31877  bj-sbceqgALT  31913  csbwrecsg  32173  poimirlem24  32427  itg2addnclem2  32456  ftc1anclem1  32479  areacirclem1  32494  areacirclem5  32498  metf1o  32545  isass  32639  rngosn3  32717  lsatcv0eq  33176  cmtbr2N  33382  atlatmstc  33448  1cvrco  33600  cdleme3  34366  cdleme7  34378  cdlemg10c  34769  dvhopellsm  35248  dibord  35290  dib1dim2  35299  diblsmopel  35302  dihopelvalcpre  35379  dih1dimatlem  35460  hdmap14lem13  36014  hdmapoc  36065  elrfirn  36100  jm2.19lem2  36399  pwfi2f1o  36508  proot1ex  36622  brfvidRP  36823  uneqsn  37165  ntrclsfveq  37204  ntrclskb  37211  ntrclsk3  37212  ntrneiel2  37228  k0004lem3  37291  bcc0  37385  pwpwuni  38074  rnmptpr  38177  disjinfi  38199  mapsnend  38210  infxrbnd2  38350  ltmulneg  38380  ltdiv23neg  38382  fourierdlem113  38936  isvonmbl  39352  2reu4a  39662  iccpartgtl  39789  iccpartleu  39791  iccpartgel  39792  fmtnoprmfac1  39840  fmtnoprmfac2  39842  bits0ALTV  39953  bgoldbtbndlem1  40046  pfxeq  40092  ltnltne  40192  edg0iedg0  40381  ausgrusgrb  40417  nb3grprlem2  40631  uvtxa01vtx0  40645  cplgr3v  40679  vtxd0nedgb  40725  vtxdusgr0edgnelALT  40733  1egrvtxdg0  40749  1wlkeq  40860  upgr2wlk  40898  1wlkp1lem8  40911  wwlksnextbi  41122  wspthsnwspthsnon  41144  s3wwlks2on  41182  elwwlks2  41192  elwspths2spth  41193  rusgrnumwwlkl1  41194  0pth-av  41315  upgriseupth  41397  eupth2lem2  41409  eupth2lem3lem4  41421  eupth2lem3lem6  41423  nfrgr2v  41464  frgr3v  41467  fusgr2wsp2nb  41520  fusgreg2wsp  41522  av-extwwlkfab  41542  av-numclwwlk2lem1  41554  av-frgrareggt1  41569  0nodd  41622  2nodd  41624  rngcinv  41795  rngcinvALTV  41807  ringcinv  41846  ringcinvALTV  41870  islindeps  42058  snlindsntor  42076  blen1b  42202  nn0sumshdiglem1  42235
  Copyright terms: Public domain W3C validator