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  4211  ordelinel  4683  ordunel  4810  funopg  5488  fnco  5556  resasplit  5616  fresaunres2  5618  resdif  5699  fnimapr  5790  ftpg  5919  fsnunfv  5936  fvpr1g  5940  fvpr2g  5941  f1ocnvfvb  6020  soisores  6050  f1oiso2  6075  ovig  6198  ov6g  6214  ovg  6215  frxp  6459  poxp  6461  moriotass  6582  f1ofveu  6587  onfununi  6606  smores3  6618  smoiso  6627  smoord  6630  smogt  6632  oaord  6793  oaword  6795  omord2  6813  omcan  6815  omword  6816  omwordi  6817  oneo  6827  oeord  6834  oecan  6835  oeword  6836  oewordi  6837  nnaord  6865  nnaword  6873  nnmwordi  6881  omabslem  6892  nnneo  6897  erov  7004  ecopovtrn  7010  undifixp  7101  xpdom3  7209  mapxpen  7276  dif1enOLD  7343  dif1en  7344  fimax2g  7356  unbnn  7366  fipreima  7415  suppr  7476  unwdomg  7555  epfrs  7670  tskwe  7842  dif1card  7897  infxpenlem  7900  cdaun  8057  cdaenun  8059  ficardun  8087  infcdaabs  8091  infcda  8093  infdif2  8095  infxpdom  8096  ackbij1lem9  8113  ackbij1lem16  8120  cflim2  8148  cfslb  8151  cfsmolem  8155  coftr  8158  infpssrlem4  8191  isf34lem7  8264  hsmexlem2  8312  axcc2lem  8321  axdc3lem4  8338  axcclem  8342  winainflem  8573  tskssel  8637  tskpr  8650  tskop  8651  tskint  8665  tskxp  8667  tskmap  8668  gruop  8685  grothpw  8706  grothpwex  8707  grothomex  8709  adderpqlem  8836  mulerpqlem  8837  addassnq  8840  mulassnq  8841  mulcanenq  8842  distrnq  8843  ltsonq  8851  ltanq  8853  ltmnq  8854  genpass  8891  distrlem1pr  8907  distrlem5pr  8909  ltsopr  8914  reclem3pr  8931  ltasr  8980  axlttrn  9153  axltadd  9154  lelttr  9170  mul12  9237  add12  9284  subadd  9313  addsub  9321  npncan  9328  nppcan  9329  nppcan3  9330  pnpcan  9345  pnncan  9347  ppncan  9348  subdi  9472  ltaddsub2  9508  leaddsub2  9510  receu  9672  divass  9701  div23  9702  divcan4  9708  divsubdir  9715  divcan5  9721  divdiv32  9727  divdiv2  9731  div2sub  9844  letrp1  9857  lemul1  9867  ltmulgt12  9876  lediv1  9880  ltdiv2  9900  lediv2  9905  ltdiv23  9906  lediv23  9907  lbinfmle  9968  infmrcl  9992  rpnnen1lem5  10609  xrlelttr  10751  xrre2  10763  xrmaxlt  10774  xrmaxle  10776  qsqueeze  10792  xaddass  10833  xltadd1  10840  xmulasslem3  10870  xmulass  10871  xltmul1  10876  xadddir  10880  xrsupsslem  10890  xrinfmsslem  10891  supxrun  10899  ixxdisj  10936  ixxub  10942  ixxlb  10943  ubioc1  10970  lbico1  10971  elioo5  10973  iccsupr  11002  lbicc2  11018  ubicc2  11019  iccneg  11023  icoshft  11024  icodisj  11027  snunico  11029  prunioo  11030  iccsplit  11034  iccf1o  11044  fzen  11077  fzrevral2  11137  fzshftral  11139  fzosubel2  11183  elfznelfzo  11197  modmulnn  11270  modabs  11279  moddi  11289  modsubdir  11290  exprec  11426  expdiv  11435  expubnd  11445  sqdiv  11452  bernneq2  11511  bcval3  11602  bccmpl  11605  hashgadd  11656  hashun  11661  hashunx  11665  hashbclem  11706  ccatval1  11750  ccatval2  11751  ccatass  11755  ccatopth2  11782  ccatco  11809  s2f1o  11868  shftval2  11895  mulre  11931  elicc4abs  12128  abssubge0  12136  abssuble0  12137  caubnd  12167  climbdd  12470  sin01gt0  12796  cos01gt0  12797  sin02gt0  12798  rpnnen2lem7  12825  dvdscmul  12881  dvdscmulr  12883  dvdsle  12900  dvdsleabs  12901  dvdsexp  12910  divalglem8  12925  divalgb  12929  sadass  12988  gcdass  13050  mulgcdr  13053  gcddiv  13054  qredeq  13111  qredeu  13112  euclemma  13113  prmdvdsexpb  13120  prmexpb  13122  coprimeprodsq  13188  coprimeprodsq2  13189  pythagtriplem1  13195  pythagtriplem3  13197  pythagtriplem6  13200  pythagtriplem12  13205  pythagtriplem13  13206  pythagtriplem14  13207  pythagtriplem16  13209  pythagtriplem19  13212  pythagtrip  13213  pcmul  13230  pcdiv  13231  pcqcl  13235  pcgcd1  13255  pcgcd  13256  pcfaclem  13272  ercpbl  13779  mreintcl  13825  ismred2  13833  mrcun  13852  submrc  13858  isfunc  14066  cofulid  14092  catcisolem  14266  posasymb  14414  isposi  14418  pleval2  14427  pltval3  14429  lubprop  14442  glbprop  14447  p0le  14477  latleeqm1  14513  lubss  14553  lubun  14555  clatglbss  14559  poslubdg  14580  mrelatglb0  14616  pslem  14643  spwpr4  14668  dirtr  14686  pwspjmhm  14772  gsumccat  14792  grpinvid1  14858  grpinvid2  14859  grpinvadd  14872  grpsubadd  14881  grppncan  14884  pwsinvg  14935  divssub  15005  odeq  15193  odf1o1  15211  odf1o2  15212  slwpss  15251  sylow2blem2  15260  lsmsubg  15293  lsmcom2  15294  lsmlub  15302  lsmss1  15303  lsmss2  15305  lsmass  15307  ablfaclem3  15650  mulgass2  15715  gsumdixp  15720  dvrcan1  15801  dvrcan3  15802  isabvd  15913  abvgt0  15921  abvres  15932  islss  16016  lspss  16065  lspssp  16069  lsslsp  16096  0lmhm  16121  reslmhm2b  16135  lsmcl  16160  lsmsp2  16164  lidlnegcl  16290  lidlnz  16304  aspss  16396  evlslem4  16569  coe1sclmul  16679  coe1sclmulfv  16680  coe1sclmul2  16681  xrsdsreclblem  16749  xrsdsreclb  16750  chrcong  16815  zndvds  16835  zntoslem  16842  ocvsscon  16907  basgen  17058  clsss  17123  ntrin  17130  elcls  17142  ntrcls0  17145  neiint  17173  neiss  17178  neips  17182  opnssneib  17184  innei  17194  islp2  17214  islp3  17215  restco  17233  restcls  17250  restntr  17251  ordtopn3  17265  ordtcld3  17268  iscnp  17306  cnconst2  17352  t1ficld  17396  cmpsublem  17467  cmpcld  17470  bwth  17478  clscon  17498  ptpjcn  17648  ptpjopn  17649  txcn  17663  ptrescn  17676  xkopjcn  17693  kqfeq  17761  kqfvima  17767  opnfbas  17879  filin  17891  neifil  17917  filuni  17922  cfinfil  17930  ufprim  17946  filufint  17957  ufinffr  17966  fin1aufil  17969  flimclslem  18021  flfneii  18029  fcfval  18070  alexsubALT  18087  cldsubg  18145  divstgphaus  18157  tsmsxp  18189  ustref  18253  ustelimasn  18257  ustimasn  18263  trust  18264  cfiluexsm  18325  cfiluweak  18330  psmetsym  18346  psmetlecl  18351  xmetlecl  18381  xmetsym  18382  prdsxmetlem  18403  xblcntrps  18445  xblcntr  18446  blssec  18470  blpnfctr  18471  txmetcn  18583  metusttoOLD  18592  metustto  18593  nmrpcl  18671  nm2dif  18676  nminvr  18710  nmoeq0  18775  0nmhm  18794  cnmet  18811  metds0  18885  metdscn2  18892  cnmpt2pc  18958  iihalf1  18961  iihalf2  18963  icchmeo  18971  bndth  18988  pi1xfr  19085  nmhmcn  19133  cphnmvs  19158  lmmbr2  19217  cfil3i  19227  bcthlem5  19286  resscdrg  19317  ovolfioo  19369  ovolficc  19370  ovolsscl  19387  ovolssnul  19388  ovoliunlem2  19404  volun  19444  iundisj2  19448  iunmbl2  19456  ovolioo  19467  itg2const  19635  cniccibl  19735  limcfval  19764  dvid  19809  dvnp1  19816  dvfsum2  19923  evlsval  19945  tdeglem3  19987  mdegmullem  20006  deg1scl  20041  deg1mul3le  20044  ig1pval3  20102  ig1pdvds  20104  ply1term  20128  coe1term  20182  dgradd2  20191  dvply1  20206  facth  20228  quotcan  20231  dvtaylp  20291  ptolemy  20409  sinq12gt0  20420  sincosq1eq  20425  efgh  20448  explog  20493  argrege0  20511  logimul  20514  logmul2  20516  logdiv2  20517  angcan  20649  ang180lem2  20657  ang180lem3  20658  pythag  20664  logrec  20666  isosctrlem1  20667  isosctrlem2  20668  angpieqvd  20677  mumullem2  20968  lgsval4  21105  lgsmod  21110  padicabv  21329  nbusgrafi  21463  nb3graprlem2  21466  nb3grapr  21467  nb3grapr2  21468  cusgra3v  21478  cusgrasizeindslem3  21489  spthonepeq  21592  1pthon  21596  constr2spth  21605  constr2pth  21606  2pthon  21607  3v3e3cycl1  21636  constr3lem5  21640  constr3trllem2  21643  constr3trllem3  21644  constr3trllem5  21646  vdgrf  21674  vdusgra0nedg  21684  hashnbgravd  21686  iseupa  21692  grpoinvid1  21823  grpoinvid2  21824  grpoasscan1  21830  grpoasscan2  21831  grpoinvop  21834  grpopncan  21844  grponpcan  21845  grpopnpcan2  21846  gxcl  21858  gxinv  21863  gxinv2  21864  gxsuc  21865  gxid  21866  gxnn0add  21867  gxnn0mul  21870  ablonncan  21887  issubgoi  21903  ablomul  21948  zerdivemp1  22027  rngoridfz  22028  vcsubdir  22040  vcnegsubdi2  22059  vcoprnelem  22062  isvc  22065  isnv  22096  nvscom  22115  nvmul0or  22138  nvpncan2  22142  nvaddsub4  22147  nvnncan  22149  nvdif  22159  nvpi  22160  nvabs  22167  nv1  22170  imsmetlem  22187  0oval  22294  lnon0  22304  blometi  22309  ajfval  22315  ipasslem5  22341  ajval  22368  hlipgt0  22421  ssphl  22424  hvadd12  22542  hvmulcom  22550  hvsubass  22551  hvsubdistr1  22556  hvsubdistr2  22557  hvaddcan2  22578  hvmulcan  22579  hvmulcan2  22580  hvsubcan  22581  hvsubcan2  22582  his7  22597  his2sub  22599  his2sub2  22600  bcs2  22689  bcs3  22690  hhssnv  22769  chj12  23041  spansncol  23075  cm2j  23127  homul12  23313  hoaddsub  23324  unopf1o  23424  adj2  23442  braadd  23453  kbmul  23463  eigvalcl  23469  lnopmulsubi  23484  hmopco  23531  cnlnadjlem2  23576  adjlnop  23594  leopmul  23642  leoptr  23645  hstoh  23740  strlem3a  23760  hstrlem3a  23768  cvntr  23800  dmdsl3  23823  atexch  23889  atcvatlem  23893  mdsymlem5  23915  cdj3lem2  23943  cdj3lem3  23946  iundisj2f  24035  curry2ima  24102  iocinioc2  24147  iundisj2fi  24158  divnumden2  24166  xreceu  24173  logeq0im1  24399  logccne0OLD  24400  logccne0  24401  logbid1  24403  logblt  24411  indfval  24419  measle0  24567  measres  24581  volfiniune  24591  sitgclbn  24662  cndprobtot  24699  cndprobnul  24700  cndprobprob  24701  ballotlemsgt1  24773  ballotlemrv1  24783  ballotlemrv2  24784  ballotlemfrcn0  24792  ghomgsg  25109  ghomf1olem  25110  lediv2aALT  25122  mulcan1g  25194  mulsuble0b  25198  prodfn0  25227  prodfrec  25228  ntrivcvgfvn0  25232  fprodabs  25302  fprodefsum  25303  iprodefisumlem  25322  binomrisefac  25363  dvdspw  25374  fununiq  25399  trpredpo  25518  wrecseq123  25537  wfrlem3  25545  wfrlem4  25546  wfrlem9  25551  sltres  25624  nodenselem8  25648  nocvxmin  25651  nofulllem3  25664  nofulllem4  25665  brbtwn2  25849  axcgrid  25860  axsegconlem6  25866  axsegconlem7  25867  axsegconlem8  25868  axsegconlem9  25869  axsegconlem10  25870  ax5seglem1  25872  ax5seglem2  25873  axpasch  25885  axlowdimlem14  25899  axlowdimlem16  25901  axeuclidlem  25906  axcontlem2  25909  axcontlem5  25912  lineext  26015  linecgr  26020  lineelsb2  26087  bpolycl  26103  cnicciblnc  26290  ftc1anclem7  26300  areacirclem2  26307  areacirclem4  26309  areacirclem5  26310  clsun  26345  neiin  26349  ivthALT  26352  fness  26376  neifg  26414  eltail  26417  fzmul  26458  heiborlem3  26536  exidreslem  26566  ghomco  26572  rngoneglmul  26581  zerdivemp1x  26585  isdrngo2  26588  rngogrphom  26601  smprngopr  26676  eldioph2  26834  elmapresaun  26843  dvdsrabdioph  26884  rabrenfdioph  26889  pellexlem5  26910  pellex  26912  pell14qrdivcl  26942  pell14qrgapw  26953  pellfund14gap  26964  reglogmul  26970  reglogexp  26971  monotoddzzfi  27019  monotoddzz  27020  zindbi  27023  jm2.17a  27039  jm2.17b  27040  congadd  27045  dvdsleabs2  27069  dvdsabsmod0  27071  jm2.19lem2  27075  jm2.19lem3  27076  jm2.19  27078  jm2.22  27080  jm2.23  27081  jm2.16nn0  27089  rmydioph  27099  rmxdiophlem  27100  jm3.1  27105  islssfgi  27161  pwssplit0  27178  pwssplit4  27182  uvcval  27225  uvcresum  27233  frlmsslsp  27239  f1lindf  27283  lnrfgtr  27315  hbtlem5  27323  pmtrval  27385  pmtrrn  27390  dvconstbi  27542  refsumcn  27691  fmuldfeq  27703  climsuselem1  27723  ibliccsinexp  27735  stoweidlem10  27749  stoweidlem14  27753  stoweidlem20  27759  stoweidlem22  27761  stoweidlem28  27767  stoweidlem31  27770  stoweidlem34  27773  stoweidlem56  27795  stoweidlem59  27798  sigaraf  27833  sigarmf  27834  sigarls  27837  el2xptp0  28076  otthg  28079  2f1fvneq  28095  f13dfv  28099  elovmpt3rab1  28107  leaddsuble  28114  2leaddle2  28115  elfzmlbm  28129  2elfz3nn0  28135  fz0fzdiffz0  28142  fzo1fzo0n0  28151  fzonmapblen  28157  ltdifltdiv  28171  modadd2mod  28177  modifeq2int  28184  ccatsymb  28211  swrdtrcfv  28228  swrdswrd  28233  swrdccatin12lem2  28241  swrdccatin12lem3b  28243  swrdccatin12lem3  28246  swrdccatin12lem4  28247  swrdccatin12  28248  swrdccat3  28249  swrdccat  28250  modprminv  28259  modprminveq  28260  modprm0  28262  cshwidx  28276  cshwidxm1  28279  cshwidxm  28280  cshwidxn  28281  2cshw1lem1  28282  2cshw1lem2  28283  2cshw1lem3  28284  2cshw2lem1  28286  2cshw2lem2  28287  2cshw2lem3  28288  2cshwmod  28291  2cshwid  28292  cshwleneq  28302  cshweqdif2  28304  cshweqrep  28308  cshw1  28309  cshw1v  28310  cshwssizelem4a  28317  nbfiusgrafi  28328  iswlkg  28338  wlkcomp  28339  2wlkeq  28341  usgra2wlkspthlem1  28344  usgra2wlkspth  28346  wwlkn  28364  wlkiswwlk2  28379  2wlkonot3v  28407  2spthonot3v  28408  usg2wlkonot  28415  usg2wotspth  28416  2pthwlkonot  28417  2spontn0vne  28419  usg2spthonot0  28421  nbhashnn0  28430  uvtxhashnb  28433  isrgra  28441  isrusgra  28442  cusgraiffrusgra  28451  frgra3v  28466  3vfriswmgra  28469  vdfrgra0  28486  vdgfrgra0  28487  vdn0frgrav2  28488  vdn1frgrav2  28490  frg2woteu  28518  frg2wot1  28520  frg2woteq  28523  usg2spot2nb  28528  usgreghash2spot  28532  reccot  28575  rectan  28576  chordthmALT  29119  sineq0ALT  29123  bnj553  29343  bnj966  29389  bnj967  29390  bnj1125  29435  bnj1173  29445  lubunNEW  29845  lsmsat  29880  lsmsatcv  29882  lcvexchlem4  29909  lcvexchlem5  29910  lfli  29933  lflcl  29936  lflmul  29940  lfl1  29942  eqlkr  29971  lshpkrlem4  29985  opcon3b  30068  oplecon3b  30072  oplecon1b  30073  opltcon3b  30076  opltcon1b  30077  oldmm1  30089  oldmm2  30090  oldmj1  30093  oldmj2  30094  olj01  30097  omllaw2N  30116  omllaw3  30117  cmtcomlemN  30120  omlfh1N  30130  omlfh3N  30131  cvrnbtwn2  30147  cvrnbtwn3  30148  cvrcon3b  30149  cvrnbtwn4  30151  leatb  30164  atcmp  30183  atnlt  30185  atcvreq0  30186  atncvrN  30187  atnle  30189  atlatle  30192  cvlexchb1  30202  hlrelat5N  30272  atcvr0eq  30297  lnnat  30298  atexchltN  30312  3at  30361  llnnlt  30394  lplnnlt  30436  2llnjaN  30437  2llnjN  30438  2atnelvolN  30458  lvolnltN  30489  2lplnj  30491  dalem21  30565  dalem23  30567  dalem24  30568  dalem25  30569  dalem29  30572  dalem30  30573  dalem31N  30574  dalem32  30575  dalem33  30576  dalem34  30577  dalem35  30578  dalem36  30579  dalem37  30580  dalem40  30583  dalem46  30589  dalem47  30590  dalem58  30601  dalem59  30602  pmaple  30632  pmapglbx  30640  elpaddri  30673  paddclN  30713  pmapjoin  30723  pmapjat1  30724  pmapjat2  30725  pclun2N  30770  polcon3N  30788  2polcon4bN  30789  polcon2N  30790  paddunN  30798  poldmj1N  30799  pmapj2N  30800  pmapocjN  30801  psubclinN  30819  paddatclN  30820  poml5N  30825  osumcllem3N  30829  osumcllem4N  30830  osumcllem11N  30837  pl42lem4N  30853  lhpmcvr5N  30898  lhp2at0  30903  lhpelim  30908  lhple  30913  lautco  30968  ldilco  30987  ltrncl  30996  ltrn11  30997  ltrncnvnid  30998  ltrnle  31000  ltrncnvleN  31001  ltrnm  31002  ltrnj  31003  ltrncvr  31004  ltrnval1  31005  ltrncnvatb  31009  ltrncnvel  31013  ltrneq2  31019  trlval2  31034  trlcnv  31036  trljat1  31037  trlne  31056  cdleme8  31121  cdlemefrs29pre00  31266  cdleme42a  31342  cdlemeg49lebilem  31410  cdlemg7fvbwN  31478  ltrnco  31590  trljco  31611  trljco2  31612  tgrpov  31619  tendocl  31638  tendopl2  31648  diaord  31919  cdlemm10N  31990  dibord  32031  dicvaddcl  32062  dicvscacl  32063  dihvalcqpre  32107  dihord6apre  32128  dihord3  32129  dihord4  32130  dihmeetlem1N  32162  dihglblem3N  32167  dihmeetlem2N  32171  dihlspsnssN  32204  dihlspsnat  32205  dihglblem6  32212  dochss  32237  dochshpncl  32256  dochdmj1  32262  dochkr1  32350  dochkr1OLDN  32351  lcfl6  32372  lcfrlem16  32430  hgmapval0  32767  hgmapvvlem3  32800  hdmapglem7  32804
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator