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

Theorem 3adant3 978
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 955 . 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 360    /\ w3a 937
This theorem is referenced by:  vtoclgft  3004  eqeu  3107  tpssi  3967  prnebg  3981  disjprg  4210  ordelinel  4682  ordunel  4809  funopg  5487  fnco  5555  resasplit  5615  fresaunres2  5617  resdif  5698  fnimapr  5789  ftpg  5918  fsnunfv  5935  fvpr1g  5939  fvpr2g  5940  f1ocnvfvb  6019  soisores  6049  f1oiso2  6074  ovig  6197  ov6g  6213  ovg  6214  frxp  6458  poxp  6460  moriotass  6581  f1ofveu  6586  onfununi  6605  smores3  6617  smoiso  6626  smoord  6629  smogt  6631  oaord  6792  oaword  6794  omord2  6812  omcan  6814  omword  6815  omwordi  6816  oneo  6826  oeord  6833  oecan  6834  oeword  6835  oewordi  6836  nnaord  6864  nnaword  6872  nnmwordi  6880  omabslem  6891  nnneo  6896  erov  7003  ecopovtrn  7009  undifixp  7100  xpdom3  7208  mapxpen  7275  dif1enOLD  7342  dif1en  7343  fimax2g  7355  unbnn  7365  fipreima  7414  suppr  7475  unwdomg  7554  epfrs  7669  tskwe  7839  dif1card  7894  infxpenlem  7897  cdaun  8054  cdaenun  8056  ficardun  8084  infcdaabs  8088  infcda  8090  infdif2  8092  infxpdom  8093  ackbij1lem9  8110  ackbij1lem16  8117  cflim2  8145  cfslb  8148  cfsmolem  8152  coftr  8155  infpssrlem4  8188  isf34lem7  8261  hsmexlem2  8309  axcc2lem  8318  axdc3lem4  8335  axcclem  8339  winainflem  8570  tskssel  8634  tskpr  8647  tskop  8648  tskint  8662  tskxp  8664  tskmap  8665  gruop  8682  grothpw  8703  grothpwex  8704  grothomex  8706  adderpqlem  8833  mulerpqlem  8834  addassnq  8837  mulassnq  8838  mulcanenq  8839  distrnq  8840  ltsonq  8848  ltanq  8850  ltmnq  8851  genpass  8888  distrlem1pr  8904  distrlem5pr  8906  ltsopr  8911  reclem3pr  8928  ltasr  8977  axlttrn  9150  axltadd  9151  lelttr  9167  mul12  9234  add12  9281  subadd  9310  addsub  9318  npncan  9325  nppcan  9326  nppcan3  9327  pnpcan  9342  pnncan  9344  ppncan  9345  subdi  9469  ltaddsub2  9505  leaddsub2  9507  receu  9669  divass  9698  div23  9699  divcan4  9705  divsubdir  9712  divcan5  9718  divdiv32  9724  divdiv2  9728  div2sub  9841  letrp1  9854  lemul1  9864  ltmulgt12  9873  lediv1  9877  ltdiv2  9897  lediv2  9902  ltdiv23  9903  lediv23  9904  lbinfmle  9965  infmrcl  9989  rpnnen1lem5  10606  xrlelttr  10748  xrre2  10760  xrmaxlt  10771  xrmaxle  10773  qsqueeze  10789  xaddass  10830  xltadd1  10837  xmulasslem3  10867  xmulass  10868  xltmul1  10873  xadddir  10877  xrsupsslem  10887  xrinfmsslem  10888  supxrun  10896  ixxdisj  10933  ixxub  10939  ixxlb  10940  ubioc1  10967  lbico1  10968  elioo5  10970  iccsupr  10999  lbicc2  11015  ubicc2  11016  iccneg  11020  icoshft  11021  icodisj  11024  snunico  11026  prunioo  11027  iccsplit  11031  iccf1o  11041  fzen  11074  fzrevral2  11134  fzshftral  11136  fzosubel2  11180  elfznelfzo  11194  modmulnn  11267  modabs  11276  moddi  11286  modsubdir  11287  exprec  11423  expdiv  11432  expubnd  11442  sqdiv  11449  bernneq2  11508  bcval3  11599  bccmpl  11602  hashgadd  11653  hashun  11658  hashunx  11662  hashbclem  11703  ccatval1  11747  ccatval2  11748  ccatass  11752  ccatopth2  11779  ccatco  11806  s2f1o  11865  shftval2  11892  mulre  11928  elicc4abs  12125  abssubge0  12133  abssuble0  12134  caubnd  12164  climbdd  12467  sin01gt0  12793  cos01gt0  12794  sin02gt0  12795  rpnnen2lem7  12822  dvdscmul  12878  dvdscmulr  12880  dvdsle  12897  dvdsleabs  12898  dvdsexp  12907  divalglem8  12922  divalgb  12926  sadass  12985  gcdass  13047  mulgcdr  13050  gcddiv  13051  qredeq  13108  qredeu  13109  euclemma  13110  prmdvdsexpb  13117  prmexpb  13119  coprimeprodsq  13185  coprimeprodsq2  13186  pythagtriplem1  13192  pythagtriplem3  13194  pythagtriplem6  13197  pythagtriplem12  13202  pythagtriplem13  13203  pythagtriplem14  13204  pythagtriplem16  13206  pythagtriplem19  13209  pythagtrip  13210  pcmul  13227  pcdiv  13228  pcqcl  13232  pcgcd1  13252  pcgcd  13253  pcfaclem  13269  ercpbl  13776  mreintcl  13822  ismred2  13830  mrcun  13849  submrc  13855  isfunc  14063  cofulid  14089  catcisolem  14263  posasymb  14411  isposi  14415  pleval2  14424  pltval3  14426  lubprop  14439  glbprop  14444  p0le  14474  latleeqm1  14510  lubss  14550  lubun  14552  clatglbss  14556  poslubdg  14577  mrelatglb0  14613  pslem  14640  spwpr4  14665  dirtr  14683  pwspjmhm  14769  gsumccat  14789  grpinvid1  14855  grpinvid2  14856  grpinvadd  14869  grpsubadd  14878  grppncan  14881  pwsinvg  14932  divssub  15002  odeq  15190  odf1o1  15208  odf1o2  15209  slwpss  15248  sylow2blem2  15257  lsmsubg  15290  lsmcom2  15291  lsmlub  15299  lsmss1  15300  lsmss2  15302  lsmass  15304  ablfaclem3  15647  mulgass2  15712  gsumdixp  15717  dvrcan1  15798  dvrcan3  15799  isabvd  15910  abvgt0  15918  abvres  15929  islss  16013  lspss  16062  lspssp  16066  lsslsp  16093  0lmhm  16118  reslmhm2b  16132  lsmcl  16157  lsmsp2  16161  lidlnegcl  16287  lidlnz  16301  aspss  16393  evlslem4  16566  coe1sclmul  16676  coe1sclmulfv  16677  coe1sclmul2  16678  xrsdsreclblem  16746  xrsdsreclb  16747  chrcong  16812  zndvds  16832  zntoslem  16839  ocvsscon  16904  basgen  17055  clsss  17120  ntrin  17127  elcls  17139  ntrcls0  17142  neiint  17170  neiss  17175  neips  17179  opnssneib  17181  innei  17191  islp2  17211  islp3  17212  restco  17230  restcls  17247  restntr  17248  ordtopn3  17262  ordtcld3  17265  iscnp  17303  cnconst2  17349  t1ficld  17393  cmpsublem  17464  cmpcld  17467  bwth  17475  clscon  17495  ptpjcn  17645  ptpjopn  17646  txcn  17660  ptrescn  17673  xkopjcn  17690  kqfeq  17758  kqfvima  17764  opnfbas  17876  filin  17888  neifil  17914  filuni  17919  cfinfil  17927  ufprim  17943  filufint  17954  ufinffr  17963  fin1aufil  17966  flimclslem  18018  flfneii  18026  fcfval  18067  alexsubALT  18084  cldsubg  18142  divstgphaus  18154  tsmsxp  18186  ustref  18250  ustelimasn  18254  ustimasn  18260  trust  18261  cfiluexsm  18322  cfiluweak  18327  psmetsym  18343  psmetlecl  18348  xmetlecl  18378  xmetsym  18379  prdsxmetlem  18400  xblcntrps  18442  xblcntr  18443  blssec  18467  blpnfctr  18468  txmetcn  18580  metusttoOLD  18589  metustto  18590  nmrpcl  18668  nm2dif  18673  nminvr  18707  nmoeq0  18772  0nmhm  18791  cnmet  18808  metds0  18882  metdscn2  18889  cnmpt2pc  18955  iihalf1  18958  iihalf2  18960  icchmeo  18968  bndth  18985  pi1xfr  19082  nmhmcn  19130  cphnmvs  19155  lmmbr2  19214  cfil3i  19224  bcthlem5  19283  resscdrg  19314  ovolfioo  19366  ovolficc  19367  ovolsscl  19384  ovolssnul  19385  ovoliunlem2  19401  volun  19441  iundisj2  19445  iunmbl2  19453  ovolioo  19464  itg2const  19634  cniccibl  19734  limcfval  19761  dvid  19806  dvnp1  19813  dvfsum2  19920  evlsval  19942  tdeglem3  19984  mdegmullem  20003  deg1scl  20038  deg1mul3le  20041  ig1pval3  20099  ig1pdvds  20101  ply1term  20125  coe1term  20179  dgradd2  20188  dvply1  20203  facth  20225  quotcan  20228  dvtaylp  20288  ptolemy  20406  sinq12gt0  20417  sincosq1eq  20422  efgh  20445  explog  20490  argrege0  20508  logimul  20511  logmul2  20513  logdiv2  20514  angcan  20646  ang180lem2  20654  ang180lem3  20655  pythag  20661  logrec  20663  isosctrlem1  20664  isosctrlem2  20665  angpieqvd  20674  mumullem2  20965  lgsval4  21102  lgsmod  21107  padicabv  21326  nbusgrafi  21460  nb3graprlem2  21463  nb3grapr  21464  nb3grapr2  21465  cusgra3v  21475  cusgrasizeindslem3  21486  spthonepeq  21589  1pthon  21593  constr2spth  21602  constr2pth  21603  2pthon  21604  3v3e3cycl1  21633  constr3lem5  21637  constr3trllem2  21640  constr3trllem3  21641  constr3trllem5  21643  vdgrf  21671  vdusgra0nedg  21681  hashnbgravd  21683  iseupa  21689  grpoinvid1  21820  grpoinvid2  21821  grpoasscan1  21827  grpoasscan2  21828  grpoinvop  21831  grpopncan  21841  grponpcan  21842  grpopnpcan2  21843  gxcl  21855  gxinv  21860  gxinv2  21861  gxsuc  21862  gxid  21863  gxnn0add  21864  gxnn0mul  21867  ablonncan  21884  issubgoi  21900  ablomul  21945  zerdivemp1  22024  rngoridfz  22025  vcsubdir  22037  vcnegsubdi2  22056  vcoprnelem  22059  isvc  22062  isnv  22093  nvscom  22112  nvmul0or  22135  nvpncan2  22139  nvaddsub4  22144  nvnncan  22146  nvdif  22156  nvpi  22157  nvabs  22164  nv1  22167  imsmetlem  22184  0oval  22291  lnon0  22301  blometi  22306  ajfval  22312  ipasslem5  22338  ajval  22365  hlipgt0  22418  ssphl  22421  hvadd12  22539  hvmulcom  22547  hvsubass  22548  hvsubdistr1  22553  hvsubdistr2  22554  hvaddcan2  22575  hvmulcan  22576  hvmulcan2  22577  hvsubcan  22578  hvsubcan2  22579  his7  22594  his2sub  22596  his2sub2  22597  bcs2  22686  bcs3  22687  hhssnv  22766  chj12  23038  spansncol  23072  cm2j  23124  homul12  23310  hoaddsub  23321  unopf1o  23421  adj2  23439  braadd  23450  kbmul  23460  eigvalcl  23466  lnopmulsubi  23481  hmopco  23528  cnlnadjlem2  23573  adjlnop  23591  leopmul  23639  leoptr  23642  hstoh  23737  strlem3a  23757  hstrlem3a  23765  cvntr  23797  dmdsl3  23820  atexch  23886  atcvatlem  23890  mdsymlem5  23912  cdj3lem2  23940  cdj3lem3  23943  iundisj2f  24032  curry2ima  24099  iocinioc2  24144  iundisj2fi  24155  divnumden2  24163  xreceu  24170  logeq0im1  24396  logccne0OLD  24397  logccne0  24398  logbid1  24400  logblt  24408  indfval  24416  measle0  24564  measres  24578  volfiniune  24588  sitgclbn  24659  cndprobtot  24696  cndprobnul  24697  cndprobprob  24698  ballotlemsgt1  24770  ballotlemrv1  24780  ballotlemrv2  24781  ballotlemfrcn0  24789  ghomgsg  25106  ghomf1olem  25107  lediv2aALT  25119  mulcan1g  25191  mulsuble0b  25195  prodfn0  25224  prodfrec  25225  ntrivcvgfvn0  25229  fprodabs  25299  fprodefsum  25300  iprodefisumlem  25319  binomrisefac  25360  dvdspw  25371  fununiq  25396  trpredpo  25515  wrecseq123  25534  wfrlem3  25542  wfrlem4  25543  wfrlem9  25548  sltres  25621  nodenselem8  25645  nocvxmin  25648  nofulllem3  25661  nofulllem4  25662  brbtwn2  25846  axcgrid  25857  axsegconlem6  25863  axsegconlem7  25864  axsegconlem8  25865  axsegconlem9  25866  axsegconlem10  25867  ax5seglem1  25869  ax5seglem2  25870  axpasch  25882  axlowdimlem14  25896  axlowdimlem16  25898  axeuclidlem  25903  axcontlem2  25906  axcontlem5  25909  lineext  26012  linecgr  26017  lineelsb2  26084  bpolycl  26100  cnicciblnc  26278  ftc1anclem7  26288  areacirclem2  26295  areacirclem4  26297  areacirclem5  26298  clsun  26333  neiin  26337  ivthALT  26340  fness  26364  neifg  26402  eltail  26405  fzmul  26446  heiborlem3  26524  exidreslem  26554  ghomco  26560  rngoneglmul  26569  zerdivemp1x  26573  isdrngo2  26576  rngogrphom  26589  smprngopr  26664  eldioph2  26822  elmapresaun  26831  dvdsrabdioph  26872  rabrenfdioph  26877  pellexlem5  26898  pellex  26900  pell14qrdivcl  26930  pell14qrgapw  26941  pellfund14gap  26952  reglogmul  26958  reglogexp  26959  monotoddzzfi  27007  monotoddzz  27008  zindbi  27011  jm2.17a  27027  jm2.17b  27028  congadd  27033  dvdsleabs2  27057  dvdsabsmod0  27059  jm2.19lem2  27063  jm2.19lem3  27064  jm2.19  27066  jm2.22  27068  jm2.23  27069  jm2.16nn0  27077  rmydioph  27087  rmxdiophlem  27088  jm3.1  27093  islssfgi  27149  pwssplit0  27166  pwssplit4  27170  uvcval  27213  uvcresum  27221  frlmsslsp  27227  f1lindf  27271  lnrfgtr  27303  hbtlem5  27311  pmtrval  27373  pmtrrn  27378  dvconstbi  27530  refsumcn  27679  fmuldfeq  27691  climsuselem1  27711  ibliccsinexp  27723  stoweidlem10  27737  stoweidlem14  27741  stoweidlem20  27747  stoweidlem22  27749  stoweidlem28  27755  stoweidlem31  27758  stoweidlem34  27761  stoweidlem56  27783  stoweidlem59  27786  sigaraf  27821  sigarmf  27822  sigarls  27825  el2xptp0  28064  otthg  28067  2f1fvneq  28083  f13dfv  28087  elovmpt3rab1  28095  leaddsuble  28102  2leaddle2  28103  elfzmlbm  28117  2elfz3nn0  28123  fz0fzdiffz0  28130  fzo1fzo0n0  28139  fzonmapblen  28145  ltdifltdiv  28159  modadd2mod  28165  modifeq2int  28172  ccatsymb  28199  swrdtrcfv  28216  swrdswrd  28221  swrdccatin12lem2  28229  swrdccatin12lem3b  28231  swrdccatin12lem3  28234  swrdccatin12lem4  28235  swrdccatin12  28236  swrdccat3  28237  swrdccat  28238  modprminv  28247  modprminveq  28248  modprm0  28250  cshwidx  28264  cshwidxm1  28267  cshwidxm  28268  cshwidxn  28269  2cshw1lem1  28270  2cshw1lem2  28271  2cshw1lem3  28272  2cshw2lem1  28274  2cshw2lem2  28275  2cshw2lem3  28276  2cshwmod  28279  2cshwid  28280  cshwleneq  28290  cshweqdif2  28292  cshweqrep  28296  cshw1  28297  cshw1v  28298  cshwssizelem4a  28305  nbfiusgrafi  28316  iswlkg  28326  wlkcomp  28327  2wlkeq  28329  usgra2wlkspthlem1  28332  usgra2wlkspth  28334  wwlkn  28352  wlkiswwlk2  28367  2wlkonot3v  28395  2spthonot3v  28396  usg2wlkonot  28403  usg2wotspth  28404  2pthwlkonot  28405  2spontn0vne  28407  usg2spthonot0  28409  nbhashnn0  28418  uvtxhashnb  28421  isrgra  28429  isrusgra  28430  cusgraiffrusgra  28439  frgra3v  28454  3vfriswmgra  28457  vdfrgra0  28474  vdgfrgra0  28475  vdn0frgrav2  28476  vdn1frgrav2  28478  frg2woteu  28506  frg2wot1  28508  frg2woteq  28511  usg2spot2nb  28516  usgreghash2spot  28520  reccot  28563  rectan  28564  chordthmALT  29107  sineq0ALT  29111  bnj553  29331  bnj966  29377  bnj967  29378  bnj1125  29423  bnj1173  29433  lubunNEW  29833  lsmsat  29868  lsmsatcv  29870  lcvexchlem4  29897  lcvexchlem5  29898  lfli  29921  lflcl  29924  lflmul  29928  lfl1  29930  eqlkr  29959  lshpkrlem4  29973  opcon3b  30056  oplecon3b  30060  oplecon1b  30061  opltcon3b  30064  opltcon1b  30065  oldmm1  30077  oldmm2  30078  oldmj1  30081  oldmj2  30082  olj01  30085  omllaw2N  30104  omllaw3  30105  cmtcomlemN  30108  omlfh1N  30118  omlfh3N  30119  cvrnbtwn2  30135  cvrnbtwn3  30136  cvrcon3b  30137  cvrnbtwn4  30139  leatb  30152  atcmp  30171  atnlt  30173  atcvreq0  30174  atncvrN  30175  atnle  30177  atlatle  30180  cvlexchb1  30190  hlrelat5N  30260  atcvr0eq  30285  lnnat  30286  atexchltN  30300  3at  30349  llnnlt  30382  lplnnlt  30424  2llnjaN  30425  2llnjN  30426  2atnelvolN  30446  lvolnltN  30477  2lplnj  30479  dalem21  30553  dalem23  30555  dalem24  30556  dalem25  30557  dalem29  30560  dalem30  30561  dalem31N  30562  dalem32  30563  dalem33  30564  dalem34  30565  dalem35  30566  dalem36  30567  dalem37  30568  dalem40  30571  dalem46  30577  dalem47  30578  dalem58  30589  dalem59  30590  pmaple  30620  pmapglbx  30628  elpaddri  30661  paddclN  30701  pmapjoin  30711  pmapjat1  30712  pmapjat2  30713  pclun2N  30758  polcon3N  30776  2polcon4bN  30777  polcon2N  30778  paddunN  30786  poldmj1N  30787  pmapj2N  30788  pmapocjN  30789  psubclinN  30807  paddatclN  30808  poml5N  30813  osumcllem3N  30817  osumcllem4N  30818  osumcllem11N  30825  pl42lem4N  30841  lhpmcvr5N  30886  lhp2at0  30891  lhpelim  30896  lhple  30901  lautco  30956  ldilco  30975  ltrncl  30984  ltrn11  30985  ltrncnvnid  30986  ltrnle  30988  ltrncnvleN  30989  ltrnm  30990  ltrnj  30991  ltrncvr  30992  ltrnval1  30993  ltrncnvatb  30997  ltrncnvel  31001  ltrneq2  31007  trlval2  31022  trlcnv  31024  trljat1  31025  trlne  31044  cdleme8  31109  cdlemefrs29pre00  31254  cdleme42a  31330  cdlemeg49lebilem  31398  cdlemg7fvbwN  31466  ltrnco  31578  trljco  31599  trljco2  31600  tgrpov  31607  tendocl  31626  tendopl2  31636  diaord  31907  cdlemm10N  31978  dibord  32019  dicvaddcl  32050  dicvscacl  32051  dihvalcqpre  32095  dihord6apre  32116  dihord3  32117  dihord4  32118  dihmeetlem1N  32150  dihglblem3N  32155  dihmeetlem2N  32159  dihlspsnssN  32192  dihlspsnat  32193  dihglblem6  32200  dochss  32225  dochshpncl  32244  dochdmj1  32250  dochkr1  32338  dochkr1OLDN  32339  lcfl6  32360  lcfrlem16  32418  hgmapval0  32755  hgmapvvlem3  32788  hdmapglem7  32792
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator