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

Theorem 3ad2ant3 978
Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
Hypothesis
Ref Expression
3ad2ant.1  |-  ( ph  ->  ch )
Assertion
Ref Expression
3ad2ant3  |-  ( ( ps  /\  th  /\  ph )  ->  ch )

Proof of Theorem 3ad2ant3
StepHypRef Expression
1 3ad2ant.1 . . 3  |-  ( ph  ->  ch )
21adantl 452 . 2  |-  ( ( th  /\  ph )  ->  ch )
323adant1 973 1  |-  ( ( ps  /\  th  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simp3l  983  simp3r  984  simp31  991  simp32  992  simp33  993  simp3ll  1026  simp3lr  1027  simp3rl  1028  simp3rr  1029  simp3l1  1060  simp3l2  1061  simp3l3  1062  simp3r1  1063  simp3r2  1064  simp3r3  1065  simp31l  1078  simp31r  1079  simp32l  1080  simp32r  1081  simp33l  1082  simp33r  1083  simp311  1102  simp312  1103  simp313  1104  simp321  1105  simp322  1106  simp323  1107  simp331  1108  simp332  1109  simp333  1110  3anim123i  1137  3jaao  1249  ceqsalt  2823  ceqsralt  2824  vtoclgft  2847  epne3  4588  limsuc  4656  poltletr  5094  funprg  5317  fsnunf  5734  fsnunfv  5736  fnsuppres  5748  weniso  5868  smoel  6393  smoord  6398  omwordi  6585  oneo  6595  oeord  6602  oewordi  6605  nnmwordi  6649  nnneo  6665  undifixp  6868  domss2  7036  domssex2  7037  unxpdomlem3  7085  dif1enOLD  7106  dif1en  7107  dffi2  7192  unwdomg  7314  ixpiunwdom  7321  oemapvali  7402  en3lplem1  7432  fodomfi2  7703  infcdaabs  7848  infunabs  7849  infdif  7851  ackbij1lem9  7870  ackbij1lem16  7877  coflim  7903  cfsmolem  7912  isfin2-2  7961  fin1a2lem9  8050  hsmexlem2  8069  axcc2lem  8078  axcc3  8080  domtriomlem  8084  axdc3lem4  8095  axcclem  8099  zornn0g  8148  axacndlem4  8248  axacndlem5  8249  axacnd  8250  gchdomtri  8267  fpwwe  8284  tskssel  8395  tskint  8423  tskurn  8427  gruurn  8436  gruixp  8447  grudomon  8455  gruina  8456  adderpqlem  8594  mulerpqlem  8595  addassnq  8598  mulassnq  8599  distrnq  8601  ltsonq  8609  ltanq  8611  ltmnq  8612  reclem3pr  8689  addid2  9011  addcan2  9013  divdir  9463  divcan5  9478  ltdiv1  9636  infmrcl  9749  infmrlb  9751  lt2halves  9962  zdivmul  10100  xaddass  10585  xleadd1  10591  xltadd1  10592  xmulasslem3  10622  xmulass  10623  xlemul1  10626  xlemul2  10627  xltmul1  10628  xadddir  10632  elioo5  10724  iccsupr  10752  iccneg  10773  icoshft  10774  icoshftf1o  10775  iccsplit  10784  fzen  10827  fzrevral  10882  fzshftral  10885  elfzo  10893  modabs  11013  modcyc  11015  moddi  11023  modsubdir  11024  expdiv  11168  leexp2a  11173  bcval3  11335  hashgadd  11375  hashfun  11405  ccatval1  11447  ccatval2  11448  ccatval3  11449  ccatass  11452  swrdval2  11469  splval  11482  ccatco  11506  swrds2  11576  sqr0  11743  elicc4abs  11819  mulcn2  12085  demoivreALT  12497  rpnnen2lem4  12512  dvdsval2  12550  dvdsexp  12600  mulgcd  12741  mulgcdr  12743  gcddiv  12744  rpmulgcd  12750  rplpwr  12751  prmexpb  12812  rpexp  12815  coprimeprodsq  12878  pythagtriplem1  12885  pythagtriplem3  12887  pythagtriplem10  12889  pythagtriplem6  12890  pythagtriplem11  12894  pythagtriplem12  12895  pythagtriplem13  12896  pythagtriplem15  12898  pythagtriplem17  12900  pythagtriplem19  12902  pcdvdsb  12937  pcfaclem  12962  vdwapun  13037  ramval  13071  0ram2  13084  0ramcl  13086  imasaddvallem  13447  imasvscaval  13456  mreiincl  13514  mremre  13522  mrieqv2d  13557  cofurid  13781  xpcpropd  13998  clatleglb  14246  gsumccat  14480  mulgdirlem  14607  mulgp1  14609  eqglact  14684  mndodcongi  14874  oddvdsnn0  14875  odngen  14904  gexnnod  14915  lsmlub  14990  lsmass  14995  efgsval2  15058  efgsrel  15059  ghmplusg  15154  odadd1  15156  odadd2  15157  gsumsn  15236  dvrcan1  15489  dvrcan3  15490  irredrmul  15505  srngadd  15638  srngmul  15639  lmhmvsca  15818  reslmhm2  15826  lbspss  15851  lsmsp  15855  lspsneu  15892  lidldvgen  16023  psropprmul  16332  coe1add  16357  coe1addfv  16358  coe1subfv  16359  coe1tm  16365  coe1sclmul  16374  coe1sclmul2  16376  cssmre  16609  iuncld  16798  clsss  16807  ntrcls0  16829  iscldtop  16848  neiss  16862  neips  16866  restcldi  16920  cnpnei  17009  cnconst2  17027  cnpresti  17032  sslm  17043  cnt0  17090  cnt1  17094  cnhaus  17098  cncmp  17135  cmpcld  17145  cnconn  17164  concompss  17175  elptr  17284  upxp  17333  qtoptop2  17406  ordthmeolem  17508  opnfbas  17553  isfil2  17567  fbasweak  17576  snfbas  17577  fgss  17584  fgcl  17589  fbasrn  17595  trnei  17603  cfinfil  17604  csdfil  17605  supfil  17606  filufint  17631  fin1aufil  17643  fmval  17654  fmf  17656  elfm  17658  elfm3  17661  imaelfm  17662  rnelfmlem  17663  rnelfm  17664  flimclslem  17695  flfneii  17703  cnpfcfi  17751  alexsubALT  17761  ptcmplem3  17764  prdsxmetlem  17948  txmetcn  18110  nmmtri  18159  nmrtri  18161  unitnmn0  18195  nminvr  18196  nmotri  18264  nghmplusg  18265  isclmi  18591  fmcfil  18714  srabn  18793  itgconst  19189  dvn2bss  19295  evlsval  19419  evlsval2  19420  deg1mul3  19517  deg1mul3le  19518  deg1tmle  19519  q1peqb  19556  r1pcl  19559  r1pdeglt  19560  r1pid  19561  dvdsq1p  19562  dvdsr1p  19563  ptolemy  19880  sincosq1eq  19896  cxplt2  20061  pythag  20131  bcmono  20532  efexple  20536  lgsdirnn0  20594  selberglem3  20712  gxpval  20942  gxnval  20943  gxnn0neg  20946  gxnn0suc  20947  gxneg  20949  gxsuc  20955  gxnn0add  20957  gxadd  20958  gxsub  20959  gxnn0mul  20960  gxmul  20961  gxmodid  20962  gxdi  20979  vcid  21123  vcdi  21124  vcdir  21125  vcass  21126  imsmetlem  21275  0oval  21382  ajval  21456  shlub  22009  hmopco  22619  adjlnop  22682  mdslmd4i  22929  ballotlemieq  23091  ballotlemrv1  23095  logeq0im1  23411  sigaclcuni  23494  measxun  23554  measvuni  23557  ind1  23617  ind0  23618  erdszelem2  23738  cnpcon  23776  cvmscld  23819  ghomf1olem  24016  dedekind  24097  faclimlem5  24121  faclim  24126  dvdspw  24174  dfon2lem3  24212  dfon2lem7  24216  predpo  24255  frrlem4  24355  nofulllem3  24429  brbtwn2  24605  axcgrid  24616  ax5seglem1  24628  ax5seglem2  24629  ax5seg  24638  axpasch  24641  axlowdimlem16  24657  axcontlem7  24670  btwndiff  24722  brcolinear2  24753  btwnconn1  24796  nnssi3  24967  nndivsub  24968  areacirclem4  25030  areacirclem6  25033  areacirc  25034  oprssopvg  25137  uninqs  25142  inttrp  25211  mapmapmap  25251  injsurinj  25252  iscst4  25280  labs1  25291  labs2  25293  isoriso2  25316  int2pre  25340  ubpar  25364  supaub  25376  inposet  25381  toplat  25393  prsubrtr  25502  zerdivemp1  25539  rngoridfz  25540  svli2  25587  npmp  25624  intopcoaconlem3b  25641  conttnf2  25665  cmptdst  25671  limptlimpr2lem2  25678  flfnei2  25680  islimrs  25683  islimrs3  25684  nolimf2  25723  lvsovso  25729  supnufb  25733  claddrv  25750  claddrvr  25751  addassv  25759  addcanri  25769  negveud  25771  negveudr  25772  issubrv  25775  mulmulvec  25790  distsava  25792  divclcvd  25797  divclrvd  25798  icccon4  25805  cmppfd  25848  1cat  25862  imonclem  25916  ismonc  25917  iepiclem  25926  isepic  25927  vtarsu  25989  vtarl  25990  tartarmap  25991  cmp2morpcats  26064  cmppar3  26077  isconc3  26111  pgapspf2  26156  isconcl5ab  26205  isibg1a6  26228  segline  26244  pxysxy  26245  lppotos  26247  bsstrs  26249  nbssntrs  26250  bosser  26270  pdiveql  26271  isibcg  26294  nn0prpwlem  26341  hmeoclda  26354  hmeocldb  26355  ivthALT  26361  ssref  26386  fnemeet1  26418  fnejoin1  26420  upixp  26506  filbcmb  26535  cnresima  26587  smprngopr  26780  igenval2  26794  ismrcd1  26876  istopclsd  26878  ismrc  26879  mapfzcons  26896  eldioph2  26944  diophrex  26958  diophren  26999  pellexlem1  27017  pellexlem5  27021  pellqrexplicit  27065  reglogmul  27081  reglogexp  27082  rmxycomplete  27105  congmul  27157  congabseq  27164  acongsym  27166  acongneg2  27167  fzneg  27172  acongeq  27173  jm2.19  27189  jm2.22  27191  jm2.23  27192  jm2.20nn  27193  rmydioph  27210  rmxdiophlem  27211  jm3.1  27216  pwssplit3  27293  pwssplit4  27294  frlmup4  27356  enfixsn  27360  mapfien2  27361  islindf2  27387  lindsind2  27392  f1lindf  27395  lindsss  27397  f1linds  27398  lindsmm  27401  lbslcic  27414  hbtlem2  27431  mndvcl  27549  mndvass  27550  mhmvlin  27555  idomrootle  27614  dvconstbi  27654  expgrowth  27655  fmul01lt1lem1  27817  climsuselem1  27836  climsuse  27837  stoweidlem3  27855  stoweidlem16  27868  stoweidlem17  27869  stoweidlem26  27878  stoweidlem34  27886  stoweidlem57  27909  f1oun2prg  28187  hashtpg  28217  nbusgra  28277  nb3graprlem1  28287  nb3graprlem2  28288  cusgra2v  28297  cusgra3v  28299  iswlkon  28332  constr3lem4  28393  constr3trllem2  28397  constr3trllem5  28400  constr3pthlem2  28402  3vfriswmgralem  28428  3vfriswmgra  28429  chordthmALT  29026  bnj837  29107  bnj517  29233  bnj553  29246  bnj594  29260  bnj967  29293  bnj1097  29327  bnj1110  29328  bnj1118  29330  bnj1128  29336  bnj1125  29338  bnj1145  29339  bnj1136  29343  bnj1173  29348  bnj1189  29355  bnj1204  29358  bnj1279  29364  bnj1321  29373  bnj1413  29381  lsmsat  29820  lsmsatcv  29822  lsatcvatlem  29861  islshpcv  29865  l1cvpat  29866  lfli  29873  lshpset2N  29931  cvrnbtwn  30083  meetat2  30109  atcmp  30123  atcvreq0  30126  atlatmstc  30131  cvlcvr1  30151  cvlcvrp  30152  cvlatcvr2  30154  cvr2N  30222  cvratlem  30232  2atjm  30256  athgt  30267  2lplnmN  30370  2llnmj  30371  2lplnmj  30433  dalemswapyzps  30501  dalem23  30507  dalem24  30508  dalem25  30509  dalem27  30510  dalem28  30511  dalem38  30521  dalem39  30522  dalem44  30527  dalem45  30528  dalem51  30534  dalem52  30535  dalem56  30539  pmapglbx  30580  pmapjat1  30664  pmapjat2  30665  paddatclN  30760  osumcllem4N  30770  osumcllem7N  30773  ltrncoval  30956  cdleme0aa  31021  cdleme0b  31023  cdleme8  31061  cdlemesner  31107  cdleme22eALTN  31156  cdleme26eALTN  31172  cdleme35h  31267  cdleme50trn2  31362  cdleme  31371  tgrpov  31559  tendotp  31572  tendoidcl  31580  tendo0co2  31599  cdlemkvcl  31653  dvhopvadd  31905  dvhopellsm  31929  dihmeetlem1N  32102  dihmeetlem9N  32127  dihatexv  32150  lcfl7lem  32311  mapdrvallem2  32457  mapdh9a  32602  hdmapevec  32650
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