MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3adant3 Structured version   Unicode version

Theorem 3adant3 977
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
Hypothesis
Ref Expression
3adant.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
3adant3  |-  ( (
ph  /\  ps  /\  th )  ->  ch )

Proof of Theorem 3adant3
StepHypRef Expression
1 3simpa 954 . 2  |-  ( (
ph  /\  ps  /\  th )  ->  ( ph  /\  ps ) )
2 3adant.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl 16 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  vtoclgft  2994  eqeu  3097  tpssi  3957  prnebg  3971  disjprg  4200  ordelinel  4672  ordunel  4799  funopg  5477  fnco  5545  resasplit  5605  fresaunres2  5607  resdif  5688  fnimapr  5779  ftpg  5908  fsnunfv  5925  fvpr1g  5929  fvpr2g  5930  f1ocnvfvb  6009  soisores  6039  f1oiso2  6064  ovig  6187  ov6g  6203  ovg  6204  frxp  6448  poxp  6450  moriotass  6571  f1ofveu  6576  onfununi  6595  smores3  6607  smoiso  6616  smoord  6619  smogt  6621  oaord  6782  oaword  6784  omord2  6802  omcan  6804  omword  6805  omwordi  6806  oneo  6816  oeord  6823  oecan  6824  oeword  6825  oewordi  6826  nnaord  6854  nnaword  6862  nnmwordi  6870  omabslem  6881  nnneo  6886  erov  6993  ecopovtrn  6999  undifixp  7090  xpdom3  7198  mapxpen  7265  dif1enOLD  7332  dif1en  7333  fimax2g  7345  unbnn  7355  fipreima  7404  suppr  7465  unwdomg  7544  epfrs  7659  tskwe  7829  dif1card  7884  infxpenlem  7887  cdaun  8044  cdaenun  8046  ficardun  8074  infcdaabs  8078  infcda  8080  infdif2  8082  infxpdom  8083  ackbij1lem9  8100  ackbij1lem16  8107  cflim2  8135  cfslb  8138  cfsmolem  8142  coftr  8145  infpssrlem4  8178  isf34lem7  8251  hsmexlem2  8299  axcc2lem  8308  axdc3lem4  8325  axcclem  8329  winainflem  8560  tskssel  8624  tskpr  8637  tskop  8638  tskint  8652  tskxp  8654  tskmap  8655  gruop  8672  grothpw  8693  grothpwex  8694  grothomex  8696  adderpqlem  8823  mulerpqlem  8824  addassnq  8827  mulassnq  8828  mulcanenq  8829  distrnq  8830  ltsonq  8838  ltanq  8840  ltmnq  8841  genpass  8878  distrlem1pr  8894  distrlem5pr  8896  ltsopr  8901  reclem3pr  8918  ltasr  8967  axlttrn  9140  axltadd  9141  lelttr  9157  mul12  9224  add12  9271  subadd  9300  addsub  9308  npncan  9315  nppcan  9316  nppcan3  9317  pnpcan  9332  pnncan  9334  ppncan  9335  subdi  9459  ltaddsub2  9495  leaddsub2  9497  receu  9659  divass  9688  div23  9689  divcan4  9695  divsubdir  9702  divcan5  9708  divdiv32  9714  divdiv2  9718  div2sub  9831  letrp1  9844  lemul1  9854  ltmulgt12  9863  lediv1  9867  ltdiv2  9887  lediv2  9892  ltdiv23  9893  lediv23  9894  lbinfmle  9955  infmrcl  9979  rpnnen1lem5  10596  xrlelttr  10738  xrre2  10750  xrmaxlt  10761  xrmaxle  10763  qsqueeze  10779  xaddass  10820  xltadd1  10827  xmulasslem3  10857  xmulass  10858  xltmul1  10863  xadddir  10867  xrsupsslem  10877  xrinfmsslem  10878  supxrun  10886  ixxdisj  10923  ixxub  10929  ixxlb  10930  ubioc1  10957  lbico1  10958  elioo5  10960  iccsupr  10989  lbicc2  11005  ubicc2  11006  iccneg  11010  icoshft  11011  icodisj  11014  snunico  11016  prunioo  11017  iccsplit  11021  iccf1o  11031  fzen  11064  fzrevral2  11124  fzshftral  11126  fzosubel2  11170  elfznelfzo  11184  modmulnn  11257  modabs  11266  moddi  11276  modsubdir  11277  exprec  11413  expdiv  11422  expubnd  11432  sqdiv  11439  bernneq2  11498  bcval3  11589  bccmpl  11592  hashgadd  11643  hashun  11648  hashunx  11652  hashbclem  11693  ccatval1  11737  ccatval2  11738  ccatass  11742  ccatopth2  11769  ccatco  11796  s2f1o  11855  shftval2  11882  mulre  11918  elicc4abs  12115  abssubge0  12123  abssuble0  12124  caubnd  12154  climbdd  12457  sin01gt0  12783  cos01gt0  12784  sin02gt0  12785  rpnnen2lem7  12812  dvdscmul  12868  dvdscmulr  12870  dvdsle  12887  dvdsleabs  12888  dvdsexp  12897  divalglem8  12912  divalgb  12916  sadass  12975  gcdass  13037  mulgcdr  13040  gcddiv  13041  qredeq  13098  qredeu  13099  euclemma  13100  prmdvdsexpb  13107  prmexpb  13109  coprimeprodsq  13175  coprimeprodsq2  13176  pythagtriplem1  13182  pythagtriplem3  13184  pythagtriplem6  13187  pythagtriplem12  13192  pythagtriplem13  13193  pythagtriplem14  13194  pythagtriplem16  13196  pythagtriplem19  13199  pythagtrip  13200  pcmul  13217  pcdiv  13218  pcqcl  13222  pcgcd1  13242  pcgcd  13243  pcfaclem  13259  ercpbl  13766  mreintcl  13812  ismred2  13820  mrcun  13839  submrc  13845  isfunc  14053  cofulid  14079  catcisolem  14253  posasymb  14401  isposi  14405  pleval2  14414  pltval3  14416  lubprop  14429  glbprop  14434  p0le  14464  latleeqm1  14500  lubss  14540  lubun  14542  clatglbss  14546  poslubdg  14567  mrelatglb0  14603  pslem  14630  spwpr4  14655  dirtr  14673  pwspjmhm  14759  gsumccat  14779  grpinvid1  14845  grpinvid2  14846  grpinvadd  14859  grpsubadd  14868  grppncan  14871  pwsinvg  14922  divssub  14992  odeq  15180  odf1o1  15198  odf1o2  15199  slwpss  15238  sylow2blem2  15247  lsmsubg  15280  lsmcom2  15281  lsmlub  15289  lsmss1  15290  lsmss2  15292  lsmass  15294  ablfaclem3  15637  mulgass2  15702  gsumdixp  15707  dvrcan1  15788  dvrcan3  15789  isabvd  15900  abvgt0  15908  abvres  15919  islss  16003  lspss  16052  lspssp  16056  lsslsp  16083  0lmhm  16108  reslmhm2b  16122  lsmcl  16147  lsmsp2  16151  lidlnegcl  16277  lidlnz  16291  aspss  16383  evlslem4  16556  coe1sclmul  16666  coe1sclmulfv  16667  coe1sclmul2  16668  xrsdsreclblem  16736  xrsdsreclb  16737  chrcong  16802  zndvds  16822  zntoslem  16829  ocvsscon  16894  basgen  17045  clsss  17110  ntrin  17117  elcls  17129  ntrcls0  17132  neiint  17160  neiss  17165  neips  17169  opnssneib  17171  innei  17181  islp2  17201  islp3  17202  restco  17220  restcls  17237  restntr  17238  ordtopn3  17252  ordtcld3  17255  iscnp  17293  cnconst2  17339  t1ficld  17383  cmpsublem  17454  cmpcld  17457  bwth  17465  clscon  17485  ptpjcn  17635  ptpjopn  17636  txcn  17650  ptrescn  17663  xkopjcn  17680  kqfeq  17748  kqfvima  17754  opnfbas  17866  filin  17878  neifil  17904  filuni  17909  cfinfil  17917  ufprim  17933  filufint  17944  ufinffr  17953  fin1aufil  17956  flimclslem  18008  flfneii  18016  fcfval  18057  alexsubALT  18074  cldsubg  18132  divstgphaus  18144  tsmsxp  18176  ustref  18240  ustelimasn  18244  ustimasn  18250  trust  18251  cfiluexsm  18312  cfiluweak  18317  psmetsym  18333  psmetlecl  18338  xmetlecl  18368  xmetsym  18369  prdsxmetlem  18390  xblcntrps  18432  xblcntr  18433  blssec  18457  blpnfctr  18458  txmetcn  18570  metusttoOLD  18579  metustto  18580  nmrpcl  18658  nm2dif  18663  nminvr  18697  nmoeq0  18762  0nmhm  18781  cnmet  18798  metds0  18872  metdscn2  18879  cnmpt2pc  18945  iihalf1  18948  iihalf2  18950  icchmeo  18958  bndth  18975  pi1xfr  19072  nmhmcn  19120  cphnmvs  19145  lmmbr2  19204  cfil3i  19214  bcthlem5  19273  resscdrg  19304  ovolfioo  19356  ovolficc  19357  ovolsscl  19374  ovolssnul  19375  ovoliunlem2  19391  volun  19431  iundisj2  19435  iunmbl2  19443  ovolioo  19454  itg2const  19624  cniccibl  19724  limcfval  19751  dvid  19796  dvnp1  19803  dvfsum2  19910  evlsval  19932  tdeglem3  19974  mdegmullem  19993  deg1scl  20028  deg1mul3le  20031  ig1pval3  20089  ig1pdvds  20091  ply1term  20115  coe1term  20169  dgradd2  20178  dvply1  20193  facth  20215  quotcan  20218  dvtaylp  20278  ptolemy  20396  sinq12gt0  20407  sincosq1eq  20412  efgh  20435  explog  20480  argrege0  20498  logimul  20501  logmul2  20503  logdiv2  20504  angcan  20636  ang180lem2  20644  ang180lem3  20645  pythag  20651  logrec  20653  isosctrlem1  20654  isosctrlem2  20655  angpieqvd  20664  mumullem2  20955  lgsval4  21092  lgsmod  21097  padicabv  21316  nbusgrafi  21450  nb3graprlem2  21453  nb3grapr  21454  nb3grapr2  21455  cusgra3v  21465  cusgrasizeindslem3  21476  spthonepeq  21579  1pthon  21583  constr2spth  21592  constr2pth  21593  2pthon  21594  3v3e3cycl1  21623  constr3lem5  21627  constr3trllem2  21630  constr3trllem3  21631  constr3trllem5  21633  vdgrf  21661  vdusgra0nedg  21671  hashnbgravd  21673  iseupa  21679  grpoinvid1  21810  grpoinvid2  21811  grpoasscan1  21817  grpoasscan2  21818  grpoinvop  21821  grpopncan  21831  grponpcan  21832  grpopnpcan2  21833  gxcl  21845  gxinv  21850  gxinv2  21851  gxsuc  21852  gxid  21853  gxnn0add  21854  gxnn0mul  21857  ablonncan  21874  issubgoi  21890  ablomul  21935  zerdivemp1  22014  rngoridfz  22015  vcsubdir  22027  vcnegsubdi2  22046  vcoprnelem  22049  isvc  22052  isnv  22083  nvscom  22102  nvmul0or  22125  nvpncan2  22129  nvaddsub4  22134  nvnncan  22136  nvdif  22146  nvpi  22147  nvabs  22154  nv1  22157  imsmetlem  22174  0oval  22281  lnon0  22291  blometi  22296  ajfval  22302  ipasslem5  22328  ajval  22355  hlipgt0  22408  ssphl  22411  hvadd12  22529  hvmulcom  22537  hvsubass  22538  hvsubdistr1  22543  hvsubdistr2  22544  hvaddcan2  22565  hvmulcan  22566  hvmulcan2  22567  hvsubcan  22568  hvsubcan2  22569  his7  22584  his2sub  22586  his2sub2  22587  bcs2  22676  bcs3  22677  hhssnv  22756  chj12  23028  spansncol  23062  cm2j  23114  homul12  23300  hoaddsub  23311  unopf1o  23411  adj2  23429  braadd  23440  kbmul  23450  eigvalcl  23456  lnopmulsubi  23471  hmopco  23518  cnlnadjlem2  23563  adjlnop  23581  leopmul  23629  leoptr  23632  hstoh  23727  strlem3a  23747  hstrlem3a  23755  cvntr  23787  dmdsl3  23810  atexch  23876  atcvatlem  23880  mdsymlem5  23902  cdj3lem2  23930  cdj3lem3  23933  iundisj2f  24022  curry2ima  24089  iocinioc2  24134  iundisj2fi  24145  divnumden2  24153  xreceu  24160  logeq0im1  24386  logccne0OLD  24387  logccne0  24388  logbid1  24390  logblt  24398  indfval  24406  measle0  24554  measres  24568  volfiniune  24578  sitgclbn  24649  cndprobtot  24686  cndprobnul  24687  cndprobprob  24688  ballotlemsgt1  24760  ballotlemrv1  24770  ballotlemrv2  24771  ballotlemfrcn0  24779  ghomgsg  25096  ghomf1olem  25097  lediv2aALT  25109  mulcan1g  25181  mulsuble0b  25185  prodfn0  25214  prodfrec  25215  ntrivcvgfvn0  25219  fprodabs  25289  fprodefsum  25290  iprodefisumlem  25309  binomrisefac  25350  dvdspw  25361  fununiq  25386  trpredpo  25505  wrecseq123  25524  wfrlem3  25532  wfrlem4  25533  wfrlem9  25538  sltres  25611  nodenselem8  25635  nocvxmin  25638  nofulllem3  25651  nofulllem4  25652  brbtwn2  25836  axcgrid  25847  axsegconlem6  25853  axsegconlem7  25854  axsegconlem8  25855  axsegconlem9  25856  axsegconlem10  25857  ax5seglem1  25859  ax5seglem2  25860  axpasch  25872  axlowdimlem14  25886  axlowdimlem16  25888  axeuclidlem  25893  axcontlem2  25896  axcontlem5  25899  lineext  26002  linecgr  26007  lineelsb2  26074  bpolycl  26090  cnicciblnc  26266  ftc1anclem7  26276  areacirclem4  26284  areacirclem5  26286  areacirclem6  26287  clsun  26322  neiin  26326  ivthALT  26329  fness  26353  neifg  26391  eltail  26394  fzmul  26435  heiborlem3  26513  exidreslem  26543  ghomco  26549  rngoneglmul  26558  zerdivemp1x  26562  isdrngo2  26565  rngogrphom  26578  smprngopr  26653  eldioph2  26811  elmapresaun  26820  dvdsrabdioph  26861  rabrenfdioph  26866  pellexlem5  26887  pellex  26889  pell14qrdivcl  26919  pell14qrgapw  26930  pellfund14gap  26941  reglogmul  26947  reglogexp  26948  monotoddzzfi  26996  monotoddzz  26997  zindbi  27000  jm2.17a  27016  jm2.17b  27017  congadd  27022  dvdsleabs2  27046  dvdsabsmod0  27048  jm2.19lem2  27052  jm2.19lem3  27053  jm2.19  27055  jm2.22  27057  jm2.23  27058  jm2.16nn0  27066  rmydioph  27076  rmxdiophlem  27077  jm3.1  27082  islssfgi  27138  pwssplit0  27155  pwssplit4  27159  uvcval  27202  uvcresum  27210  frlmsslsp  27216  f1lindf  27260  lnrfgtr  27292  hbtlem5  27300  pmtrval  27362  pmtrrn  27367  dvconstbi  27519  refsumcn  27668  fmuldfeq  27680  climsuselem1  27700  ibliccsinexp  27712  stoweidlem10  27726  stoweidlem14  27730  stoweidlem20  27736  stoweidlem22  27738  stoweidlem28  27744  stoweidlem31  27747  stoweidlem34  27750  stoweidlem56  27772  stoweidlem59  27775  sigaraf  27810  sigarmf  27811  sigarls  27814  el2xptp0  28051  otthg  28054  2f1fvneq  28063  f13dfv  28067  leaddsuble  28076  2leaddle2  28077  elfzmlbm  28090  2elfz3nn0  28096  fz0fzdiffz0  28103  fzo1fzo0n0  28111  fzonmapblen  28117  ltdifltdiv  28126  modadd2mod  28132  modifeq2int  28139  ccatsymb  28152  swrdswrd  28165  swrdccatin12lem2  28173  swrdccatin12lem3b  28175  swrdccatin12lem3  28178  swrdccatin12lem4  28179  swrdccatin12  28180  swrdccat3  28181  swrdccat  28182  modprminv  28191  modprminveq  28192  modprm0  28194  cshwidx  28208  cshwidxm1  28211  cshwidxm  28212  cshwidxn  28213  2cshw1lem1  28214  2cshw1lem2  28215  2cshw1lem3  28216  2cshw2lem1  28218  2cshw2lem2  28219  2cshw2lem3  28220  2cshwmod  28223  2cshwid  28224  cshwleneq  28231  cshweqdif2  28233  cshweqrep  28237  cshw1  28238  cshw1v  28239  cshwssizelem4a  28246  nbfiusgrafi  28257  usgra2wlkspthlem1  28259  usgra2wlkspth  28261  2wlkonot3v  28295  2spthonot3v  28296  usg2wlkonot  28303  usg2wotspth  28304  2pthwlkonot  28305  2spontn0vne  28307  usg2spthonot0  28309  frgra3v  28329  3vfriswmgra  28332  vdfrgra0  28349  vdgfrgra0  28350  vdn0frgrav2  28351  vdn1frgrav2  28353  frg2woteu  28381  frg2wot1  28383  frg2woteq  28386  usg2spot2nb  28391  usgreghash2spot  28395  reccot  28438  rectan  28439  chordthmALT  28982  sineq0ALT  28986  bnj553  29206  bnj966  29252  bnj967  29253  bnj1125  29298  bnj1173  29308  lubunNEW  29708  lsmsat  29743  lsmsatcv  29745  lcvexchlem4  29772  lcvexchlem5  29773  lfli  29796  lflcl  29799  lflmul  29803  lfl1  29805  eqlkr  29834  lshpkrlem4  29848  opcon3b  29931  oplecon3b  29935  oplecon1b  29936  opltcon3b  29939  opltcon1b  29940  oldmm1  29952  oldmm2  29953  oldmj1  29956  oldmj2  29957  olj01  29960  omllaw2N  29979  omllaw3  29980  cmtcomlemN  29983  omlfh1N  29993  omlfh3N  29994  cvrnbtwn2  30010  cvrnbtwn3  30011  cvrcon3b  30012  cvrnbtwn4  30014  leatb  30027  atcmp  30046  atnlt  30048  atcvreq0  30049  atncvrN  30050  atnle  30052  atlatle  30055  cvlexchb1  30065  hlrelat5N  30135  atcvr0eq  30160  lnnat  30161  atexchltN  30175  3at  30224  llnnlt  30257  lplnnlt  30299  2llnjaN  30300  2llnjN  30301  2atnelvolN  30321  lvolnltN  30352  2lplnj  30354  dalem21  30428  dalem23  30430  dalem24  30431  dalem25  30432  dalem29  30435  dalem30  30436  dalem31N  30437  dalem32  30438  dalem33  30439  dalem34  30440  dalem35  30441  dalem36  30442  dalem37  30443  dalem40  30446  dalem46  30452  dalem47  30453  dalem58  30464  dalem59  30465  pmaple  30495  pmapglbx  30503  elpaddri  30536  paddclN  30576  pmapjoin  30586  pmapjat1  30587  pmapjat2  30588  pclun2N  30633  polcon3N  30651  2polcon4bN  30652  polcon2N  30653  paddunN  30661  poldmj1N  30662  pmapj2N  30663  pmapocjN  30664  psubclinN  30682  paddatclN  30683  poml5N  30688  osumcllem3N  30692  osumcllem4N  30693  osumcllem11N  30700  pl42lem4N  30716  lhpmcvr5N  30761  lhp2at0  30766  lhpelim  30771  lhple  30776  lautco  30831  ldilco  30850  ltrncl  30859  ltrn11  30860  ltrncnvnid  30861  ltrnle  30863  ltrncnvleN  30864  ltrnm  30865  ltrnj  30866  ltrncvr  30867  ltrnval1  30868  ltrncnvatb  30872  ltrncnvel  30876  ltrneq2  30882  trlval2  30897  trlcnv  30899  trljat1  30900  trlne  30919  cdleme8  30984  cdlemefrs29pre00  31129  cdleme42a  31205  cdlemeg49lebilem  31273  cdlemg7fvbwN  31341  ltrnco  31453  trljco  31474  trljco2  31475  tgrpov  31482  tendocl  31501  tendopl2  31511  diaord  31782  cdlemm10N  31853  dibord  31894  dicvaddcl  31925  dicvscacl  31926  dihvalcqpre  31970  dihord6apre  31991  dihord3  31992  dihord4  31993  dihmeetlem1N  32025  dihglblem3N  32030  dihmeetlem2N  32034  dihlspsnssN  32067  dihlspsnat  32068  dihglblem6  32075  dochss  32100  dochshpncl  32119  dochdmj1  32125  dochkr1  32213  dochkr1OLDN  32214  lcfl6  32235  lcfrlem16  32293  hgmapval0  32630  hgmapvvlem3  32663  hdmapglem7  32667
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator