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

Theorem 3adant3 975
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 952 . 2  |-  ( (
ph  /\  ps  /\  th )  ->  ( ph  /\  ps ) )
2 3adant.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl 15 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  vtoclgft  2868  eqeu  2970  disjprg  4056  ordelinel  4528  ordunel  4655  funopg  5323  fnco  5389  resasplit  5449  fresaunres2  5451  resdif  5532  fnimapr  5621  fsnunfv  5759  f1ocnvfvb  5837  soisores  5866  f1oiso2  5891  ovig  6011  ov6g  6027  ovg  6028  frxp  6267  poxp  6269  moriotass  6376  f1ofveu  6381  onfununi  6400  smores3  6412  smoiso  6421  smoord  6424  smogt  6426  oaord  6587  oaword  6589  omord2  6607  omcan  6609  omword  6610  omwordi  6611  oneo  6621  oeord  6628  oecan  6629  oeword  6630  oewordi  6631  nnaord  6659  nnaword  6667  nnmwordi  6675  omabslem  6686  nnneo  6691  erov  6798  ecopovtrn  6804  undifixp  6895  xpdom3  7003  mapxpen  7070  dif1enOLD  7135  dif1en  7136  fimax2g  7148  unbnn  7158  fipreima  7206  suppr  7264  unwdomg  7343  epfrs  7458  tskwe  7628  dif1card  7683  infxpenlem  7686  cdaun  7843  cdaenun  7845  ficardun  7873  infcdaabs  7877  infcda  7879  infdif2  7881  infxpdom  7882  ackbij1lem9  7899  ackbij1lem16  7906  cflim2  7934  cfslb  7937  cfsmolem  7941  coftr  7944  infpssrlem4  7977  isf34lem7  8050  hsmexlem2  8098  axcc2lem  8107  axdc3lem4  8124  axcclem  8128  winainflem  8360  tskssel  8424  tskpr  8437  tskop  8438  tskint  8452  tskxp  8454  tskmap  8455  gruop  8472  grothpw  8493  grothpwex  8494  grothomex  8496  adderpqlem  8623  mulerpqlem  8624  addassnq  8627  mulassnq  8628  mulcanenq  8629  distrnq  8630  ltsonq  8638  ltanq  8640  ltmnq  8641  genpass  8678  distrlem1pr  8694  distrlem5pr  8696  ltsopr  8701  reclem3pr  8718  ltasr  8767  axlttrn  8940  axltadd  8941  lelttr  8957  mul12  9023  add12  9070  subadd  9099  addsub  9107  npncan  9114  nppcan  9115  nppcan3  9116  pnpcan  9131  pnncan  9133  ppncan  9134  subdi  9258  ltaddsub2  9294  leaddsub2  9296  receu  9458  divass  9487  div23  9488  divcan4  9494  divsubdir  9501  divcan5  9507  divdiv32  9513  divdiv2  9517  div2sub  9630  letrp1  9643  lemul1  9653  ltmulgt12  9662  lediv1  9666  ltdiv2  9686  lediv2  9691  ltdiv23  9692  lediv23  9693  lbinfmle  9754  infmrcl  9778  rpnnen1lem5  10393  xrlelttr  10534  xrre2  10546  xrmaxlt  10557  xrmaxle  10559  qsqueeze  10575  xaddass  10616  xltadd1  10623  xmulasslem3  10653  xmulass  10654  xltmul1  10659  xadddir  10663  xrsupsslem  10672  xrinfmsslem  10673  supxrun  10681  ixxdisj  10718  ixxub  10724  ixxlb  10725  ubioc1  10752  lbico1  10753  elioo5  10755  iccsupr  10783  lbicc2  10799  ubicc2  10800  iccneg  10804  icoshft  10805  icodisj  10808  snunico  10810  prunioo  10811  iccsplit  10815  iccf1o  10825  fzen  10858  fzrevral2  10914  fzshftral  10916  fzosubel2  10956  modmulnn  11035  modabs  11044  moddi  11054  modsubdir  11055  exprec  11190  expdiv  11199  expubnd  11209  sqdiv  11216  bernneq2  11275  bcval3  11366  bccmpl  11369  hashgadd  11406  hashun  11411  hashbclem  11437  ccatval1  11478  ccatval2  11479  ccatass  11483  ccatopth2  11510  ccatco  11537  shftval2  11617  mulre  11653  elicc4abs  11850  abssubge0  11858  abssuble0  11859  caubnd  11889  sin01gt0  12517  cos01gt0  12518  sin02gt0  12519  rpnnen2lem7  12546  dvdscmul  12602  dvdscmulr  12604  dvdsle  12621  dvdsleabs  12622  dvdsexp  12631  divalglem8  12646  divalgb  12650  sadass  12709  gcdass  12771  mulgcdr  12774  gcddiv  12775  qredeq  12832  qredeu  12833  euclemma  12834  prmdvdsexpb  12841  prmexpb  12843  coprimeprodsq  12909  coprimeprodsq2  12910  pythagtriplem1  12916  pythagtriplem3  12918  pythagtriplem6  12921  pythagtriplem12  12926  pythagtriplem13  12927  pythagtriplem14  12928  pythagtriplem16  12930  pythagtriplem19  12933  pythagtrip  12934  pcmul  12951  pcdiv  12952  pcqcl  12956  pcgcd1  12976  pcgcd  12977  pcfaclem  12993  ercpbl  13500  mreintcl  13546  ismred2  13554  mrcun  13573  submrc  13579  isfunc  13787  cofulid  13813  catcisolem  13987  posasymb  14135  isposi  14139  pleval2  14148  pltval3  14150  lubprop  14163  glbprop  14168  p0le  14198  latleeqm1  14234  lubss  14274  lubun  14276  clatglbss  14280  poslubdg  14301  mrelatglb0  14337  pslem  14364  spwpr4  14389  dirtr  14407  pwspjmhm  14493  gsumccat  14513  grpinvid1  14579  grpinvid2  14580  grpinvadd  14593  grpsubadd  14602  grppncan  14605  pwsinvg  14656  divssub  14726  odeq  14914  odf1o1  14932  odf1o2  14933  slwpss  14972  sylow2blem2  14981  lsmsubg  15014  lsmcom2  15015  lsmlub  15023  lsmss1  15024  lsmss2  15026  lsmass  15028  ablfaclem3  15371  mulgass2  15436  gsumdixp  15441  dvrcan1  15522  dvrcan3  15523  isabvd  15634  abvgt0  15642  abvres  15653  islss  15741  lspss  15790  lspssp  15794  lsslsp  15821  0lmhm  15846  reslmhm2b  15860  lsmcl  15885  lsmsp2  15889  lidlnegcl  16015  lidlnz  16029  aspss  16121  evlslem4  16294  coe1sclmul  16407  coe1sclmulfv  16408  coe1sclmul2  16409  xrsdsreclblem  16473  xrsdsreclb  16474  chrcong  16539  zndvds  16559  zntoslem  16566  ocvsscon  16631  basgen  16782  clsss  16847  ntrin  16854  elcls  16866  ntrcls0  16869  neiint  16897  neiss  16902  neips  16906  opnssneib  16908  innei  16918  islp2  16933  restco  16951  restcls  16967  restntr  16968  ordtopn3  16982  ordtcld3  16985  iscnp  17023  cnconst2  17067  t1ficld  17111  cmpsublem  17182  cmpcld  17185  clscon  17212  ptpjcn  17361  ptpjopn  17362  txcn  17376  ptrescn  17389  xkopjcn  17406  kqfeq  17471  kqfvima  17477  opnfbas  17589  filin  17601  neifil  17627  filuni  17632  cfinfil  17640  ufprim  17656  filufint  17667  ufinffr  17676  fin1aufil  17679  flimclslem  17731  flfneii  17739  fcfval  17780  alexsubALT  17797  cldsubg  17845  divstgphaus  17857  tsmsxp  17889  xmetlecl  17963  xmetsym  17964  prdsxmetlem  17984  xblcntr  18015  blssec  18033  blpnfctr  18034  txmetcn  18146  nmrpcl  18193  nm2dif  18198  nminvr  18232  nmoeq0  18297  0nmhm  18316  cnmet  18333  metds0  18406  metdscn2  18413  cnmpt2pc  18479  iihalf1  18482  iihalf2  18484  icchmeo  18492  bndth  18509  pi1xfr  18606  nmhmcn  18654  cphnmvs  18679  lmmbr2  18738  cfil3i  18748  bcthlem5  18803  resscdrg  18828  ovolfioo  18880  ovolficc  18881  ovolsscl  18898  ovolssnul  18899  ovoliunlem2  18915  volun  18955  iundisj2  18959  iunmbl2  18967  ovolioo  18978  itg2const  19148  cniccibl  19248  limcfval  19275  dvid  19320  dvnp1  19327  dvfsum2  19434  evlsval  19456  tdeglem3  19498  mdegmullem  19517  deg1scl  19552  deg1mul3le  19555  ig1pval3  19613  ig1pdvds  19615  ply1term  19639  coe1term  19693  dgradd2  19702  dvply1  19717  facth  19739  quotcan  19742  dvtaylp  19802  ptolemy  19917  sinq12gt0  19928  sincosq1eq  19933  efgh  19956  explog  20000  argrege0  20018  logimul  20021  angcan  20153  ang180lem2  20161  ang180lem3  20162  pythag  20168  logrec  20170  isosctrlem1  20171  isosctrlem2  20172  angpieqvd  20181  mumullem2  20471  lgsval4  20608  lgsmod  20613  padicabv  20832  grpoinvid1  20950  grpoinvid2  20951  grpoasscan1  20957  grpoasscan2  20958  grpoinvop  20961  grpopncan  20971  grponpcan  20972  grpopnpcan2  20973  gxcl  20985  gxinv  20990  gxinv2  20991  gxsuc  20992  gxid  20993  gxnn0add  20994  gxnn0mul  20997  ablonncan  21014  issubgoi  21030  ablomul  21075  zerdivemp1  21154  rngoridfz  21155  vcsubdir  21167  vcnegsubdi2  21186  vcoprnelem  21189  isvc  21192  isnv  21223  nvscom  21242  nvmul0or  21265  nvpncan2  21269  nvaddsub4  21274  nvnncan  21276  nvdif  21286  nvpi  21287  nvabs  21294  nv1  21297  imsmetlem  21314  0oval  21421  lnon0  21431  blometi  21436  ajfval  21442  ipasslem5  21468  ajval  21495  hlipgt0  21548  ssphl  21551  hvadd12  21669  hvmulcom  21677  hvsubass  21678  hvsubdistr1  21683  hvsubdistr2  21684  hvaddcan2  21705  hvmulcan  21706  hvmulcan2  21707  hvsubcan  21708  hvsubcan2  21709  his7  21724  his2sub  21726  his2sub2  21727  bcs2  21816  bcs3  21817  hhssnv  21896  chj12  22168  spansncol  22202  cm2j  22254  homul12  22440  hoaddsub  22451  unopf1o  22551  adj2  22569  braadd  22580  kbmul  22590  eigvalcl  22596  lnopmulsubi  22611  hmopco  22658  cnlnadjlem2  22703  adjlnop  22721  leopmul  22769  leoptr  22772  hstoh  22867  strlem3a  22887  hstrlem3a  22895  cvntr  22927  dmdsl3  22950  atexch  23016  atcvatlem  23020  mdsymlem5  23042  cdj3lem2  23070  cdj3lem3  23073  iundisj2f  23172  curry2ima  23247  iocinioc2  23289  iundisj2fi  23302  xreceu  23320  ustref  23431  trust  23441  cfiluexsm  23482  metustto  23495  logeq0im1  23586  logccne0  23587  logccne0ALT  23588  logbid1  23590  logblt  23598  measle0  23736  measres  23750  volfiniune  23760  indfval  23829  cndprobtot  23868  cndprobprob  23870  ballotlemsgt1  23942  ballotlemrv1  23952  ballotlemrv2  23953  ballotlemfrcn0  23961  iseupa  24165  ghomgsg  24284  ghomf1olem  24285  lediv2aALT  24297  mulcan1g  24370  mulsuble0b  24374  ntrivcvgfvn0  24404  dvdspw  24488  fununiq  24511  trpredpo  24623  wfrlem3  24643  wfrlem4  24644  wfrlem9  24649  sltres  24703  nodenselem8  24727  nocvxmin  24730  nofulllem3  24743  nofulllem4  24744  brbtwn2  24919  axcgrid  24930  axsegconlem6  24936  axsegconlem7  24937  axsegconlem8  24938  axsegconlem9  24939  axsegconlem10  24940  ax5seglem1  24942  ax5seglem2  24943  axpasch  24955  axlowdimlem14  24969  axlowdimlem16  24971  axeuclidlem  24976  axcontlem2  24979  axcontlem5  24982  lineext  25085  linecgr  25090  lineelsb2  25157  bpolycl  25173  itg2addnc  25319  cnicciblnc  25336  areacirclem4  25344  areacirclem5  25346  areacirclem6  25347  clsun  25395  neiin  25399  ivthALT  25407  fness  25431  neifg  25469  eltail  25472  fimaxre2OLD  25580  fzmul  25592  lpss2  25617  heiborlem3  25685  exidreslem  25715  ghomco  25721  rngoneglmul  25730  zerdivemp1x  25734  isdrngo2  25737  rngogrphom  25750  smprngopr  25825  eldioph2  25989  elmapresaun  25998  dvdsrabdioph  26039  rabrenfdioph  26045  pellexlem5  26066  pellex  26068  pell14qrdivcl  26098  pell14qrgapw  26109  pellfund14gap  26120  reglogmul  26126  reglogexp  26127  monotoddzzfi  26175  monotoddzz  26176  zindbi  26179  jm2.17a  26195  jm2.17b  26196  congadd  26201  dvdsleabs2  26225  dvdsabsmod0  26227  jm2.19lem2  26231  jm2.19lem3  26232  jm2.19  26234  jm2.22  26236  jm2.23  26237  jm2.16nn0  26245  rmydioph  26255  rmxdiophlem  26256  jm3.1  26261  islssfgi  26318  pwssplit0  26335  pwssplit4  26339  uvcval  26382  uvcresum  26390  frlmsslsp  26396  f1lindf  26440  lnrfgtr  26472  hbtlem5  26480  pmtrval  26542  pmtrrn  26547  dvconstbi  26699  refsumcn  26849  fmuldfeq  26861  climsuselem1  26881  stoweidlem10  26907  stoweidlem14  26911  stoweidlem20  26917  stoweidlem28  26925  stoweidlem34  26931  stoweidlem51  26948  stoweidlem56  26953  stoweidlem59  26956  sigaraf  26991  sigarmf  26992  sigarls  26995  ftpg  27234  fvpr1g  27235  fvpr2g  27236  elfznelfzo  27275  hashunx  27294  s2f1o  27299  nbusgrafi  27395  nb3graprlem2  27398  nb3grapr  27399  nb3grapr2  27400  cusgra3v  27409  1pthon  27487  3v3e3cycl1  27528  constr3lem5  27532  constr3trllem2  27535  constr3trllem3  27536  constr3trllem5  27538  vdgref  27565  vdusgraval  27574  hashnbgravd  27577  frgra3v  27594  3vfriswmgra  27597  vdfrgra0  27614  vdgfrgra0  27615  vdfrgragt2  27620  reccot  27677  rectan  27678  chordthmALT  28221  bnj553  28441  bnj966  28487  bnj967  28488  bnj1125  28533  bnj1173  28543  lubunNEW  28981  lsmsat  29016  lsmsatcv  29018  lcvexchlem4  29045  lcvexchlem5  29046  lfli  29069  lflcl  29072  lflmul  29076  lfl1  29078  eqlkr  29107  lshpkrlem4  29121  opcon3b  29204  oplecon3b  29208  oplecon1b  29209  opltcon3b  29212  opltcon1b  29213  oldmm1  29225  oldmm2  29226  oldmj1  29229  oldmj2  29230  olj01  29233  omllaw2N  29252  omllaw3  29253  cmtcomlemN  29256  omlfh1N  29266  omlfh3N  29267  cvrnbtwn2  29283  cvrnbtwn3  29284  cvrcon3b  29285  cvrnbtwn4  29287  leatb  29300  atcmp  29319  atnlt  29321  atcvreq0  29322  atncvrN  29323  atnle  29325  atlatle  29328  cvlexchb1  29338  hlrelat5N  29408  atcvr0eq  29433  lnnat  29434  atexchltN  29448  3at  29497  llnnlt  29530  lplnnlt  29572  2llnjaN  29573  2llnjN  29574  2atnelvolN  29594  lvolnltN  29625  2lplnj  29627  dalem21  29701  dalem23  29703  dalem24  29704  dalem25  29705  dalem29  29708  dalem30  29709  dalem31N  29710  dalem32  29711  dalem33  29712  dalem34  29713  dalem35  29714  dalem36  29715  dalem37  29716  dalem40  29719  dalem46  29725  dalem47  29726  dalem58  29737  dalem59  29738  pmaple  29768  pmapglbx  29776  elpaddri  29809  paddclN  29849  pmapjoin  29859  pmapjat1  29860  pmapjat2  29861  pclun2N  29906  polcon3N  29924  2polcon4bN  29925  polcon2N  29926  paddunN  29934  poldmj1N  29935  pmapj2N  29936  pmapocjN  29937  psubclinN  29955  paddatclN  29956  poml5N  29961  osumcllem3N  29965  osumcllem4N  29966  osumcllem11N  29973  pl42lem4N  29989  lhpmcvr5N  30034  lhp2at0  30039  lhpelim  30044  lhple  30049  lautco  30104  ldilco  30123  ltrncl  30132  ltrn11  30133  ltrncnvnid  30134  ltrnle  30136  ltrncnvleN  30137  ltrnm  30138  ltrnj  30139  ltrncvr  30140  ltrnval1  30141  ltrncnvatb  30145  ltrncnvel  30149  ltrneq2  30155  trlval2  30170  trlcnv  30172  trljat1  30173  trlne  30192  cdleme8  30257  cdlemefrs29pre00  30402  cdleme42a  30478  cdlemeg49lebilem  30546  cdlemg7fvbwN  30614  ltrnco  30726  trljco  30747  trljco2  30748  tgrpov  30755  tendocl  30774  tendopl2  30784  diaord  31055  cdlemm10N  31126  dibord  31167  dicvaddcl  31198  dicvscacl  31199  dihvalcqpre  31243  dihord6apre  31264  dihord3  31265  dihord4  31266  dihmeetlem1N  31298  dihglblem3N  31303  dihmeetlem2N  31307  dihlspsnssN  31340  dihlspsnat  31341  dihglblem6  31348  dochss  31373  dochshpncl  31392  dochdmj1  31398  dochkr1  31486  dochkr1OLDN  31487  lcfl6  31508  lcfrlem16  31566  hgmapval0  31903  hgmapvvlem3  31936  hdmapglem7  31940
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator