MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3adant3 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  2945  eqeu  3048  prnebg  3921  disjprg  4149  ordelinel  4620  ordunel  4747  funopg  5425  fnco  5493  resasplit  5553  fresaunres2  5555  resdif  5636  fnimapr  5726  ftpg  5855  fsnunfv  5872  fvpr1g  5876  fvpr2g  5877  f1ocnvfvb  5956  soisores  5986  f1oiso2  6011  ovig  6134  ov6g  6150  ovg  6151  frxp  6392  poxp  6394  moriotass  6515  f1ofveu  6520  onfununi  6539  smores3  6551  smoiso  6560  smoord  6563  smogt  6565  oaord  6726  oaword  6728  omord2  6746  omcan  6748  omword  6749  omwordi  6750  oneo  6760  oeord  6767  oecan  6768  oeword  6769  oewordi  6770  nnaord  6798  nnaword  6806  nnmwordi  6814  omabslem  6825  nnneo  6830  erov  6937  ecopovtrn  6943  undifixp  7034  xpdom3  7142  mapxpen  7209  dif1enOLD  7276  dif1en  7277  fimax2g  7289  unbnn  7299  fipreima  7347  suppr  7406  unwdomg  7485  epfrs  7600  tskwe  7770  dif1card  7825  infxpenlem  7828  cdaun  7985  cdaenun  7987  ficardun  8015  infcdaabs  8019  infcda  8021  infdif2  8023  infxpdom  8024  ackbij1lem9  8041  ackbij1lem16  8048  cflim2  8076  cfslb  8079  cfsmolem  8083  coftr  8086  infpssrlem4  8119  isf34lem7  8192  hsmexlem2  8240  axcc2lem  8249  axdc3lem4  8266  axcclem  8270  winainflem  8501  tskssel  8565  tskpr  8578  tskop  8579  tskint  8593  tskxp  8595  tskmap  8596  gruop  8613  grothpw  8634  grothpwex  8635  grothomex  8637  adderpqlem  8764  mulerpqlem  8765  addassnq  8768  mulassnq  8769  mulcanenq  8770  distrnq  8771  ltsonq  8779  ltanq  8781  ltmnq  8782  genpass  8819  distrlem1pr  8835  distrlem5pr  8837  ltsopr  8842  reclem3pr  8859  ltasr  8908  axlttrn  9081  axltadd  9082  lelttr  9098  mul12  9164  add12  9211  subadd  9240  addsub  9248  npncan  9255  nppcan  9256  nppcan3  9257  pnpcan  9272  pnncan  9274  ppncan  9275  subdi  9399  ltaddsub2  9435  leaddsub2  9437  receu  9599  divass  9628  div23  9629  divcan4  9635  divsubdir  9642  divcan5  9648  divdiv32  9654  divdiv2  9658  div2sub  9771  letrp1  9784  lemul1  9794  ltmulgt12  9803  lediv1  9807  ltdiv2  9827  lediv2  9832  ltdiv23  9833  lediv23  9834  lbinfmle  9895  infmrcl  9919  rpnnen1lem5  10536  xrlelttr  10678  xrre2  10690  xrmaxlt  10701  xrmaxle  10703  qsqueeze  10719  xaddass  10760  xltadd1  10767  xmulasslem3  10797  xmulass  10798  xltmul1  10803  xadddir  10807  xrsupsslem  10817  xrinfmsslem  10818  supxrun  10826  ixxdisj  10863  ixxub  10869  ixxlb  10870  ubioc1  10897  lbico1  10898  elioo5  10900  iccsupr  10929  lbicc2  10945  ubicc2  10946  iccneg  10950  icoshft  10951  icodisj  10954  snunico  10956  prunioo  10957  iccsplit  10961  iccf1o  10971  fzen  11004  fzrevral2  11062  fzshftral  11064  fzosubel2  11106  elfznelfzo  11119  modmulnn  11192  modabs  11201  moddi  11211  modsubdir  11212  exprec  11348  expdiv  11357  expubnd  11367  sqdiv  11374  bernneq2  11433  bcval3  11524  bccmpl  11527  hashgadd  11578  hashun  11583  hashunx  11587  hashbclem  11628  ccatval1  11672  ccatval2  11673  ccatass  11677  ccatopth2  11704  ccatco  11731  s2f1o  11790  shftval2  11817  mulre  11853  elicc4abs  12050  abssubge0  12058  abssuble0  12059  caubnd  12089  climbdd  12392  sin01gt0  12718  cos01gt0  12719  sin02gt0  12720  rpnnen2lem7  12747  dvdscmul  12803  dvdscmulr  12805  dvdsle  12822  dvdsleabs  12823  dvdsexp  12832  divalglem8  12847  divalgb  12851  sadass  12910  gcdass  12972  mulgcdr  12975  gcddiv  12976  qredeq  13033  qredeu  13034  euclemma  13035  prmdvdsexpb  13042  prmexpb  13044  coprimeprodsq  13110  coprimeprodsq2  13111  pythagtriplem1  13117  pythagtriplem3  13119  pythagtriplem6  13122  pythagtriplem12  13127  pythagtriplem13  13128  pythagtriplem14  13129  pythagtriplem16  13131  pythagtriplem19  13134  pythagtrip  13135  pcmul  13152  pcdiv  13153  pcqcl  13157  pcgcd1  13177  pcgcd  13178  pcfaclem  13194  ercpbl  13701  mreintcl  13747  ismred2  13755  mrcun  13774  submrc  13780  isfunc  13988  cofulid  14014  catcisolem  14188  posasymb  14336  isposi  14340  pleval2  14349  pltval3  14351  lubprop  14364  glbprop  14369  p0le  14399  latleeqm1  14435  lubss  14475  lubun  14477  clatglbss  14481  poslubdg  14502  mrelatglb0  14538  pslem  14565  spwpr4  14590  dirtr  14608  pwspjmhm  14694  gsumccat  14714  grpinvid1  14780  grpinvid2  14781  grpinvadd  14794  grpsubadd  14803  grppncan  14806  pwsinvg  14857  divssub  14927  odeq  15115  odf1o1  15133  odf1o2  15134  slwpss  15173  sylow2blem2  15182  lsmsubg  15215  lsmcom2  15216  lsmlub  15224  lsmss1  15225  lsmss2  15227  lsmass  15229  ablfaclem3  15572  mulgass2  15637  gsumdixp  15642  dvrcan1  15723  dvrcan3  15724  isabvd  15835  abvgt0  15843  abvres  15854  islss  15938  lspss  15987  lspssp  15991  lsslsp  16018  0lmhm  16043  reslmhm2b  16057  lsmcl  16082  lsmsp2  16086  lidlnegcl  16212  lidlnz  16226  aspss  16318  evlslem4  16491  coe1sclmul  16601  coe1sclmulfv  16602  coe1sclmul2  16603  xrsdsreclblem  16667  xrsdsreclb  16668  chrcong  16733  zndvds  16753  zntoslem  16760  ocvsscon  16825  basgen  16976  clsss  17041  ntrin  17048  elcls  17060  ntrcls0  17063  neiint  17091  neiss  17096  neips  17100  opnssneib  17102  innei  17112  islp2  17132  restco  17150  restcls  17167  restntr  17168  ordtopn3  17182  ordtcld3  17185  iscnp  17223  cnconst2  17269  t1ficld  17313  cmpsublem  17384  cmpcld  17387  clscon  17414  ptpjcn  17564  ptpjopn  17565  txcn  17579  ptrescn  17592  xkopjcn  17609  kqfeq  17677  kqfvima  17683  opnfbas  17795  filin  17807  neifil  17833  filuni  17838  cfinfil  17846  ufprim  17862  filufint  17873  ufinffr  17882  fin1aufil  17885  flimclslem  17937  flfneii  17945  fcfval  17986  alexsubALT  18003  cldsubg  18061  divstgphaus  18073  tsmsxp  18105  ustref  18169  ustelimasn  18173  ustimasn  18179  trust  18180  cfiluexsm  18241  cfiluweak  18246  xmetlecl  18285  xmetsym  18286  prdsxmetlem  18306  xblcntr  18337  blssec  18355  blpnfctr  18356  txmetcn  18468  metustto  18473  nmrpcl  18537  nm2dif  18542  nminvr  18576  nmoeq0  18641  0nmhm  18660  cnmet  18677  metds0  18751  metdscn2  18758  cnmpt2pc  18824  iihalf1  18827  iihalf2  18829  icchmeo  18837  bndth  18854  pi1xfr  18951  nmhmcn  18999  cphnmvs  19024  lmmbr2  19083  cfil3i  19093  bcthlem5  19150  resscdrg  19179  ovolfioo  19231  ovolficc  19232  ovolsscl  19249  ovolssnul  19250  ovoliunlem2  19266  volun  19306  iundisj2  19310  iunmbl2  19318  ovolioo  19329  itg2const  19499  cniccibl  19599  limcfval  19626  dvid  19671  dvnp1  19678  dvfsum2  19785  evlsval  19807  tdeglem3  19849  mdegmullem  19868  deg1scl  19903  deg1mul3le  19906  ig1pval3  19964  ig1pdvds  19966  ply1term  19990  coe1term  20044  dgradd2  20053  dvply1  20068  facth  20090  quotcan  20093  dvtaylp  20153  ptolemy  20271  sinq12gt0  20282  sincosq1eq  20287  efgh  20310  explog  20355  argrege0  20373  logimul  20376  logmul2  20378  logdiv2  20379  angcan  20511  ang180lem2  20519  ang180lem3  20520  pythag  20526  logrec  20528  isosctrlem1  20529  isosctrlem2  20530  angpieqvd  20539  mumullem2  20830  lgsval4  20967  lgsmod  20972  padicabv  21191  nbusgrafi  21324  nb3graprlem2  21327  nb3grapr  21328  nb3grapr2  21329  cusgra3v  21339  cusgrasizeindslem3  21350  1pthon  21439  3v3e3cycl1  21479  constr3lem5  21483  constr3trllem2  21486  constr3trllem3  21487  constr3trllem5  21489  vdgrf  21517  vdusgra0nedg  21527  hashnbgravd  21529  iseupa  21535  grpoinvid1  21666  grpoinvid2  21667  grpoasscan1  21673  grpoasscan2  21674  grpoinvop  21677  grpopncan  21687  grponpcan  21688  grpopnpcan2  21689  gxcl  21701  gxinv  21706  gxinv2  21707  gxsuc  21708  gxid  21709  gxnn0add  21710  gxnn0mul  21713  ablonncan  21730  issubgoi  21746  ablomul  21791  zerdivemp1  21870  rngoridfz  21871  vcsubdir  21883  vcnegsubdi2  21902  vcoprnelem  21905  isvc  21908  isnv  21939  nvscom  21958  nvmul0or  21981  nvpncan2  21985  nvaddsub4  21990  nvnncan  21992  nvdif  22002  nvpi  22003  nvabs  22010  nv1  22013  imsmetlem  22030  0oval  22137  lnon0  22147  blometi  22152  ajfval  22158  ipasslem5  22184  ajval  22211  hlipgt0  22264  ssphl  22267  hvadd12  22385  hvmulcom  22393  hvsubass  22394  hvsubdistr1  22399  hvsubdistr2  22400  hvaddcan2  22421  hvmulcan  22422  hvmulcan2  22423  hvsubcan  22424  hvsubcan2  22425  his7  22440  his2sub  22442  his2sub2  22443  bcs2  22532  bcs3  22533  hhssnv  22612  chj12  22884  spansncol  22918  cm2j  22970  homul12  23156  hoaddsub  23167  unopf1o  23267  adj2  23285  braadd  23296  kbmul  23306  eigvalcl  23312  lnopmulsubi  23327  hmopco  23374  cnlnadjlem2  23419  adjlnop  23437  leopmul  23485  leoptr  23488  hstoh  23583  strlem3a  23603  hstrlem3a  23611  cvntr  23643  dmdsl3  23666  atexch  23732  atcvatlem  23736  mdsymlem5  23758  cdj3lem2  23786  cdj3lem3  23789  iundisj2f  23873  curry2ima  23938  iocinioc2  23978  iundisj2fi  23991  divnumden2  23999  xreceu  24006  logeq0im1  24190  logccne0OLD  24191  logccne0  24192  logbid1  24194  logblt  24202  indfval  24210  measle0  24356  measres  24370  volfiniune  24380  cndprobtot  24473  cndprobnul  24474  cndprobprob  24475  ballotlemsgt1  24547  ballotlemrv1  24557  ballotlemrv2  24558  ballotlemfrcn0  24566  ghomgsg  24883  ghomf1olem  24884  lediv2aALT  24896  mulcan1g  24968  mulsuble0b  24972  prodfn0  25001  prodfrec  25002  ntrivcvgfvn0  25006  fprodabs  25076  fprodefsum  25077  dvdspw  25127  fununiq  25150  trpredpo  25262  wfrlem3  25282  wfrlem4  25283  wfrlem9  25288  sltres  25342  nodenselem8  25366  nocvxmin  25369  nofulllem3  25382  nofulllem4  25383  brbtwn2  25558  axcgrid  25569  axsegconlem6  25575  axsegconlem7  25576  axsegconlem8  25577  axsegconlem9  25578  axsegconlem10  25579  ax5seglem1  25581  ax5seglem2  25582  axpasch  25594  axlowdimlem14  25608  axlowdimlem16  25610  axeuclidlem  25615  axcontlem2  25618  axcontlem5  25621  lineext  25724  linecgr  25729  lineelsb2  25796  bpolycl  25812  itg2addnc  25959  cnicciblnc  25976  areacirclem4  25984  areacirclem5  25986  areacirclem6  25987  clsun  26022  neiin  26026  ivthALT  26029  fness  26053  neifg  26091  eltail  26094  fzmul  26135  heiborlem3  26213  exidreslem  26243  ghomco  26249  rngoneglmul  26258  zerdivemp1x  26262  isdrngo2  26265  rngogrphom  26278  smprngopr  26353  eldioph2  26511  elmapresaun  26520  dvdsrabdioph  26561  rabrenfdioph  26566  pellexlem5  26587  pellex  26589  pell14qrdivcl  26619  pell14qrgapw  26630  pellfund14gap  26641  reglogmul  26647  reglogexp  26648  monotoddzzfi  26696  monotoddzz  26697  zindbi  26700  jm2.17a  26716  jm2.17b  26717  congadd  26722  dvdsleabs2  26746  dvdsabsmod0  26748  jm2.19lem2  26752  jm2.19lem3  26753  jm2.19  26755  jm2.22  26757  jm2.23  26758  jm2.16nn0  26766  rmydioph  26776  rmxdiophlem  26777  jm3.1  26782  islssfgi  26839  pwssplit0  26856  pwssplit4  26860  uvcval  26903  uvcresum  26911  frlmsslsp  26917  f1lindf  26961  lnrfgtr  26993  hbtlem5  27001  pmtrval  27063  pmtrrn  27068  dvconstbi  27220  refsumcn  27369  fmuldfeq  27381  climsuselem1  27401  ibliccsinexp  27413  stoweidlem10  27427  stoweidlem14  27431  stoweidlem20  27437  stoweidlem22  27439  stoweidlem28  27445  stoweidlem31  27448  stoweidlem34  27451  stoweidlem56  27473  stoweidlem59  27476  sigaraf  27511  sigarmf  27512  sigarls  27515  frgra3v  27755  3vfriswmgra  27758  vdfrgra0  27775  vdgfrgra0  27776  vdn0frgrav2  27777  vdn1frgrav2  27779  reccot  27847  rectan  27848  chordthmALT  28387  bnj553  28607  bnj966  28653  bnj967  28654  bnj1125  28699  bnj1173  28709  lubunNEW  29088  lsmsat  29123  lsmsatcv  29125  lcvexchlem4  29152  lcvexchlem5  29153  lfli  29176  lflcl  29179  lflmul  29183  lfl1  29185  eqlkr  29214  lshpkrlem4  29228  opcon3b  29311  oplecon3b  29315  oplecon1b  29316  opltcon3b  29319  opltcon1b  29320  oldmm1  29332  oldmm2  29333  oldmj1  29336  oldmj2  29337  olj01  29340  omllaw2N  29359  omllaw3  29360  cmtcomlemN  29363  omlfh1N  29373  omlfh3N  29374  cvrnbtwn2  29390  cvrnbtwn3  29391  cvrcon3b  29392  cvrnbtwn4  29394  leatb  29407  atcmp  29426  atnlt  29428  atcvreq0  29429  atncvrN  29430  atnle  29432  atlatle  29435  cvlexchb1  29445  hlrelat5N  29515  atcvr0eq  29540  lnnat  29541  atexchltN  29555  3at  29604  llnnlt  29637  lplnnlt  29679  2llnjaN  29680  2llnjN  29681  2atnelvolN  29701  lvolnltN  29732  2lplnj  29734  dalem21  29808  dalem23  29810  dalem24  29811  dalem25  29812  dalem29  29815  dalem30  29816  dalem31N  29817  dalem32  29818  dalem33  29819  dalem34  29820  dalem35  29821  dalem36  29822  dalem37  29823  dalem40  29826  dalem46  29832  dalem47  29833  dalem58  29844  dalem59  29845  pmaple  29875  pmapglbx  29883  elpaddri  29916  paddclN  29956  pmapjoin  29966  pmapjat1  29967  pmapjat2  29968  pclun2N  30013  polcon3N  30031  2polcon4bN  30032  polcon2N  30033  paddunN  30041  poldmj1N  30042  pmapj2N  30043  pmapocjN  30044  psubclinN  30062  paddatclN  30063  poml5N  30068  osumcllem3N  30072  osumcllem4N  30073  osumcllem11N  30080  pl42lem4N  30096  lhpmcvr5N  30141  lhp2at0  30146  lhpelim  30151  lhple  30156  lautco  30211  ldilco  30230  ltrncl  30239  ltrn11  30240  ltrncnvnid  30241  ltrnle  30243  ltrncnvleN  30244  ltrnm  30245  ltrnj  30246  ltrncvr  30247  ltrnval1  30248  ltrncnvatb  30252  ltrncnvel  30256  ltrneq2  30262  trlval2  30277  trlcnv  30279  trljat1  30280  trlne  30299  cdleme8  30364  cdlemefrs29pre00  30509  cdleme42a  30585  cdlemeg49lebilem  30653  cdlemg7fvbwN  30721  ltrnco  30833  trljco  30854  trljco2  30855  tgrpov  30862  tendocl  30881  tendopl2  30891  diaord  31162  cdlemm10N  31233  dibord  31274  dicvaddcl  31305  dicvscacl  31306  dihvalcqpre  31350  dihord6apre  31371  dihord3  31372  dihord4  31373  dihmeetlem1N  31405  dihglblem3N  31410  dihmeetlem2N  31414  dihlspsnssN  31447  dihlspsnat  31448  dihglblem6  31455  dochss  31480  dochshpncl  31499  dochdmj1  31505  dochkr1  31593  dochkr1OLDN  31594  lcfl6  31615  lcfrlem16  31673  hgmapval0  32010  hgmapvvlem3  32043  hdmapglem7  32047
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