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

Theorem 3bitrd 294
 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 268 . 2 (𝜑 → (𝜓𝜃))
4 3bitrd.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitrd 268 1 (𝜑 → (𝜓𝜏))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196 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 197 This theorem is referenced by:  sbceqal  3520  elimhyp3v  4181  elimhyp4v  4182  keephyp3v  4187  frsn  5223  opelresg  5434  elpredg  5732  f1eq123d  6169  foeq123d  6170  f1oeq123d  6171  fnmptfvd  6360  fnotovb  6735  ofrfval  6947  eloprabi  7277  fnmpt2ovd  7297  suppsnop  7354  smoeq  7492  infglbb  8438  wemapwe  8632  fseqenlem1  8885  dfac12lem2  9004  fin23lem22  9187  pwfseqlem5  9523  pwfseq  9524  enqbreq2  9780  lterpq  9830  ltdiv23  10952  lediv23  10953  negfi  11009  halfpos  11300  addltmul  11306  div4p1lem1div2  11325  supminf  11813  supxrbnd1  12189  supxrbnd2  12190  iccf1o  12354  fzshftral  12466  fzoshftral  12625  2tnp1ge0ge0  12670  dfceil2  12680  modirr  12781  hashen1  13198  seqcoll  13286  hash2prb  13292  hashle2prv  13298  ccat0  13394  s111  13432  swrdeq  13490  wrd2ind  13523  2swrd2eqwrdeq  13742  eqwrds3  13750  limsupgle  14252  tanaddlem  14940  dvdssub  15073  addmodlteqALT  15094  dvdsmod  15097  oddp1even  15115  nn0o1gt2  15144  nn0oddm1d2  15148  bitscmp  15207  saddisjlem  15233  smueqlem  15259  ncoprmgcdne1b  15410  cncongr1  15428  cncongr2  15429  prmreclem5  15671  4sqlem11  15706  4sqlem17  15712  vdwmc2  15730  ismre  16297  acsfn  16367  dfiso2  16479  brcic  16505  isssc  16527  setcinv  16787  intopsn  17300  sgrp1  17340  sgrp2nmndlem4  17462  nmzsubg  17682  conjnmzb  17742  gsmsymgreqlem2  17897  symgfixels  17900  f1omvdconj  17912  oddvdsnn0  18009  oddvds  18012  odcong  18014  odf1  18025  dpjeq  18504  pgpfac1lem2  18520  ring1  18648  lsmspsn  19132  lbsacsbs  19204  lpigen  19304  prmirredlem  19889  znf1o  19948  znleval  19951  znunit  19960  islinds2  20200  islindf4  20225  scmatf1  20385  isclo  20939  maxlp  20999  1stccn  21314  xkoinjcn  21538  elmptrab  21678  fbunfip  21720  elfm  21798  fmid  21811  flfnei  21842  isflf  21844  isfcls  21860  fclsopn  21865  isfcf  21885  cnextfun  21915  eltsms  21983  prdsxmetlem  22220  elmopn  22294  metss  22360  comet  22365  elbl4  22415  metuel2  22417  nrmmetd  22426  metdsge  22699  tchcph  23082  fmcfil  23116  rrxmet  23237  minveclem4  23249  shft2rab  23322  sca2rab  23326  volsup2  23419  mbfsup  23476  i1fmullem  23506  mbfi1fseqlem4  23530  xrge0f  23543  itg2monolem1  23562  ellimc2  23686  cnlimc  23697  mdegleb  23869  facth1  23969  ulm2  24184  sineq0  24318  coseq1  24319  efeq1  24320  sinord  24325  root1eq1  24541  angrtmuld  24583  quad2  24611  dcubic  24618  cubic2  24620  dquartlem1  24623  dquart  24625  quart  24633  rlimcnp  24737  lgamucov  24809  mumullem2  24951  chtub  24982  fsumvma  24983  fsumvma2  24984  chpchtsum  24989  bposlem7  25060  lgsneg  25091  lgsne0  25105  lgsprme0  25109  lgsqrlem2  25117  lgsquadlem1  25150  lgsquadlem2  25151  2lgs  25177  2lgsoddprm  25186  istrkg3ld  25405  tgcgr4  25471  iscgra1  25747  isleag  25778  iseqlg  25792  axcontlem7  25895  edg0iedg0  25994  edg0iedg0OLD  25995  ausgrusgrb  26105  usgr1v0edg  26194  nb3grprlem2  26327  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  cplgr3v  26387  vtxd0nedgb  26440  vtxdusgr0edgnelALT  26448  1egrvtxdg0  26463  wlkeq  26585  upgr2wlk  26620  wlkp1lem8  26633  wwlksnextbi  26857  wspthsnwspthsnonOLD  26881  s3wwlks2on  26922  elwwlks2  26933  elwspths2spth  26934  rusgrnumwwlkl1  26935  0pth  27103  upgriseupth  27185  eupth2lem2  27197  eupth2lem3lem4  27209  eupth2lem3lem6  27211  nfrgr2v  27252  frgr3v  27255  fusgr2wsp2nb  27314  fusgreg2wsp  27316  extwwlkfab  27342  numclwwlk2lem1  27356  numclwwlk2lem1OLD  27363  frgrreggt1  27380  imsmetlem  27673  ipz  27702  bnsscmcl  27852  minvecolem4  27864  hvsubcan  28059  hoeq2  28818  leoptri  29123  atcv0eq  29366  elimifd  29488  gtiso  29606  2ndpreima  29613  fpwrelmapffslem  29635  fzsplit3  29681  isomnd  29829  ogrpinvlt  29852  smatrcl  29990  pstmfval  30067  lmlim  30121  dya2ub  30460  eulerpartlemr  30564  isrrvv  30633  ballotlemsima  30705  signsvfn  30787  subfacp1lem3  31290  subfacp1lem5  31292  erdszelem1  31299  erdsze  31310  erdsze2lem2  31312  filnetlem4  32501  bj-issetwt  32984  bj-sbceqgALT  33022  bj-raldifsn  33179  csbwrecsg  33303  poimirlem24  33563  itg2addnclem2  33592  ftc1anclem1  33615  areacirclem1  33630  areacirclem5  33634  metf1o  33681  isass  33775  rngosn3  33853  brxrn  34276  lsatcv0eq  34652  cmtbr2N  34858  atlatmstc  34924  1cvrco  35076  cdleme3  35842  cdleme7  35854  cdlemg10c  36244  dvhopellsm  36723  dibord  36765  dib1dim2  36774  diblsmopel  36777  dihopelvalcpre  36854  dih1dimatlem  36935  hdmap14lem13  37489  hdmapoc  37540  elrfirn  37575  jm2.19lem2  37874  pwfi2f1o  37983  proot1ex  38096  brfvidRP  38297  uneqsn  38638  ntrclsfveq  38677  ntrclskb  38684  ntrclsk3  38685  ntrneiel2  38701  k0004lem3  38764  bcc0  38856  pwpwuni  39539  rnmptpr  39672  disjinfi  39694  mapsnend  39705  rnmptbd2  39778  rnmptbd  39785  infxrbnd2  39898  ltmulneg  39928  ltdiv23neg  39930  rexabsle  39959  uzub  39971  supxrleubrnmptf  39993  supminfxr  40007  limsupre2lem  40274  limsupre2mpt  40280  limsupre3mpt  40284  limsupreuz  40287  limsuplt2  40303  liminflimsupclim  40357  xlimclim  40368  xlimbr  40371  xlimclim2lem  40383  xlimmnfmpt  40387  xlimpnfmpt  40388  fourierdlem113  40754  isvonmbl  41173  2reu4a  41510  ltnltne  41638  iccpartgtl  41687  iccpartleu  41689  iccpartgel  41690  pfxeq  41729  fmtnoprmfac1  41802  fmtnoprmfac2  41804  bits0ALTV  41915  bgoldbtbndlem1  42018  0nodd  42135  2nodd  42137  rngcinv  42306  rngcinvALTV  42318  ringcinv  42357  ringcinvALTV  42381  islindeps  42567  snlindsntor  42585  blen1b  42707  nn0sumshdiglem1  42740
 Copyright terms: Public domain W3C validator