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

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

Proof of Theorem 3ad2ant2
StepHypRef Expression
1 3ad2ant.1 . . 3  |-  ( ph  ->  ch )
21adantr 451 . 2  |-  ( (
ph  /\  th )  ->  ch )
323adant1 973 1  |-  ( ( ps  /\  ph  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simp2l  981  simp2r  982  simp21  988  simp22  989  simp23  990  simp2ll  1022  simp2lr  1023  simp2rl  1024  simp2rr  1025  simp2l1  1054  simp2l2  1055  simp2l3  1056  simp2r1  1057  simp2r2  1058  simp2r3  1059  simp21l  1072  simp21r  1073  simp22l  1074  simp22r  1075  simp23l  1076  simp23r  1077  simp211  1093  simp212  1094  simp213  1095  simp221  1096  simp222  1097  simp223  1098  simp231  1099  simp232  1100  simp233  1101  3anim123i  1137  3jaao  1249  ceqsalt  2823  vtoclgft  2847  vtoclegft  2868  epne3  4588  sofld  5137  fnprg  5321  fnco  5368  fvun1  5606  fsnunf2  5735  oprssov  6005  sorpssuni  6302  sorpssint  6303  onfununi  6374  onoviun  6376  smogt  6400  omass  6594  f1dom2g  6895  domunfican  7145  dffi2  7192  ordiso2  7246  wemapso  7282  unwdomg  7314  wdomima2g  7316  ixpiunwdom  7321  cantnfres  7395  dif1card  7654  ackbij1lem9  7870  ackbij1lem16  7877  cfflb  7901  coflim  7903  cfsmolem  7912  fincssdom  7965  isf32lem11  8005  domtriomlem  8084  axdc4lem  8097  ac6num  8122  axacndlem4  8248  axacndlem5  8249  axacnd  8250  elwina  8324  elina  8325  winaon  8326  inawina  8328  winacard  8330  winainflem  8331  tsksuc  8400  tskuni  8421  grupr  8435  nqereu  8569  enqeq  8574  nqereq  8575  adderpqlem  8594  mulerpqlem  8595  addassnq  8598  mulassnq  8599  distrnq  8601  ltsonq  8609  ltanq  8611  ltmnq  8612  div2neg  9499  lediv2  9662  nndivtr  9803  zdivmul  10100  gtndiv  10105  fzind  10126  eluzp1p1  10269  peano2uz  10288  xrre2  10515  xaddass  10585  xlt2add  10596  xmulasslem3  10622  xmulass  10623  supxrun  10650  icc0  10720  ubioc1  10721  ubicc2  10769  iccsplit  10784  elfzo0  10920  modabs  11013  modcyc  11015  moddi  11023  modsubdir  11024  expneg2  11128  expnbnd  11246  digit2  11250  hashgadd  11375  hashfun  11405  ccatval3  11449  ccatass  11452  swrd00  11467  swrdval2  11469  swrdlen  11472  ccatopth  11478  ccatopth2  11479  ccatco  11506  swrds2  11576  rediv  11632  imdiv  11639  resqrex  11752  resqrcl  11755  limsupgle  11967  climuni  12042  mulcn2  12085  iseraltlem3  12172  rpnnen2lem7  12515  divalglem8  12615  ndvdssub  12622  bitsfzo  12642  mulgcd  12741  mulgcdr  12743  gcddiv  12744  rplpwr  12751  rppwr  12752  qredeq  12801  pythagtriplem1  12885  pythagtriplem3  12887  pythagtriplem10  12889  pythagtriplem6  12890  pythagtriplem7  12891  pythagtriplem11  12894  pythagtriplem12  12895  pythagtriplem13  12896  pythagtriplem14  12897  pythagtriplem16  12899  pythagtriplem19  12902  pythagtrip  12903  pcfaclem  12962  pcbc  12964  vdwapun  13037  vdwapid1  13038  imasaddvallem  13447  ismre  13508  mreincl  13517  submre  13523  mrcss  13534  comfeq  13625  cofurid  13781  xpcpropd  13998  issubmnd  14417  frmdup3  14504  cycsubg2cl  14671  ghmnsgima  14722  mndodcongi  14874  oddvdsnn0  14875  oddvds  14878  odeq  14881  odmulg2  14884  odmulg  14885  odhash2  14902  odhash3  14903  gexnnod  14915  gexcl2  14916  isslw  14935  subgslw  14943  oppglsm  14969  lsmsubm  14980  lsmless1  14986  lsmless2  14987  lsmass  14995  efgsval2  15058  efgsrel  15059  efgsfo  15064  ghmplusg  15154  odadd1  15156  odadd2  15157  gsumconst  15225  gsumsn  15236  ablfac1eu  15324  pgpfac1lem5  15330  ablfaclem3  15338  rngidss  15383  irredrmul  15505  abvres  15620  srngadd  15638  srngmul  15639  lssincl  15738  lsslsp  15788  reslmhm2b  15827  lsmsp  15855  sralmod  15955  aspid  16086  asclmul1  16095  asclmul2  16096  coe1add  16357  coe1addfv  16358  coe1subfv  16359  ntrin  16814  elnei  16864  restco  16911  restcldi  16920  sslm  17043  cnt1  17094  cmpsublem  17142  cmpcld  17145  kgen2ss  17266  upxp  17333  xkopjcn  17366  xkococnlem  17369  xkococn  17370  qtopval2  17403  qtoptop2  17406  ordthmeolem  17508  isfil2  17567  fgss  17584  fbasrn  17595  ufilmax  17618  filufint  17631  fmval  17654  elfm2  17659  elfm3  17661  rnelfmlem  17663  rnelfm  17664  flimrest  17694  flfnei  17702  isflf  17704  flffbas  17706  fclsrest  17735  cnpfcfi  17751  alexsubALTlem4  17760  subgntr  17805  opnsubg  17806  tgpconcompss  17812  divstgpopn  17818  divstgphaus  17821  blres  17993  metcnp3  18102  nmmtri  18159  nmrtri  18161  nminvr  18196  nmotri  18264  nghmplusg  18265  tgqioo  18322  iccpnfhmeo  18459  caun0  18723  pjth  18819  volsup2  18976  itg2le  19110  dvn2bss  19295  evlsval2  19420  mdegldg  19468  mdegnn0cl  19473  deg1ldgdomn  19496  deg1mul3  19517  drnguc1p  19572  ig1peu  19573  ig1pdvds  19578  coeid3  19638  coe11  19650  dgradd2  19665  facth  19702  dvtaylp  19765  pserdvlem2  19820  ptolemy  19880  tanord1  19915  cxple2  20060  cxpeq  20113  isosctrlem2  20135  muval1  20387  dvdssqf  20392  chpwordi  20411  efchtdvds  20413  logfacbnd3  20478  bcmono  20532  efexple  20536  lgslem1  20551  lgsneg  20574  lgssq2  20591  lgsdirnn0  20594  dchrmusumlema  20658  selberglem3  20712  pntrmax  20729  padicabv  20795  gxmodid  20962  resgrprn  20963  ghomid  21048  nvsge0  21245  nmoub2i  21368  isblo3i  21395  dipassr2  21441  bcs2  21777  elspansn2  22162  fh2  22214  pjoi0  22312  homco2  22573  leopmul  22730  cdj3lem2  23031  ballotlemsgt1  23085  ballotlemieq  23091  ballotlemfrcn0  23104  rexdiv  23125  unitdivcld  23300  relogbcl  23419  sigaclcuni  23494  probun  23637  cnpcon  23776  cvmsf1o  23818  cvmscld  23819  cvmlift2lem6  23854  ghomfo  24013  modaddabs  24026  faclimlem5  24121  dfrdg2  24223  frrlem5e  24360  nobndlem8  24424  nofulllem2  24428  brbtwn2  24605  ax5seglem2  24629  ax5seglem3  24631  axlowdim  24661  axcontlem7  24670  axcontlem8  24671  fvtransport  24727  nndivsub  24968  itg2addnclem  25003  itg2addnc  25005  iccss3  25237  injsurinj  25252  valcurfn1  25307  int2pre  25340  supwval  25387  dfps2  25392  clfsebsr  25452  fprodadd  25455  fprodneg  25481  fprodsub  25482  prsubrtr  25502  mulveczer  25582  mulinvsca  25583  svli2  25587  svs2  25590  truni1  25608  truni3  25610  intfmu2  25622  npmp  25624  cmptdst  25671  prdnei  25676  islimrs4  25685  mslb1  25710  2wsms  25711  lvsovso  25729  supnufb  25733  claddrv  25750  claddrvr  25751  addassv  25759  negveud  25771  negveudr  25772  issubrv  25775  idosd  25847  dmrngcmp  25854  1cat  25862  imonclem  25916  cmpmon  25918  icmpmon  25919  idmon  25920  isepic  25927  morsubc  25958  vtarl  25990  tartarmap  25991  fnctartar2  26011  codcatfun  26037  cmp2morpcats  26064  cmppar3  26077  isconc3  26111  clscnc  26113  isconcl5ab  26205  bsstrs  26249  nbssntrs  26250  bosser  26270  pdiveql  26271  isibcg  26294  nn0prpwlem  26341  nn0prpw  26342  ivthALT  26361  fness  26385  topmeet  26416  fnejoin1  26420  f1ocan1fv  26497  f1ocan2fv  26498  upixp  26506  filbcmb  26535  mettrifi  26576  rngohom0  26706  rngohomsub  26707  rngokerinj  26709  intidl  26757  keridl  26760  nacsfix  26890  mapco2g  26893  mapfzcons  26896  mzpexpmpt  26926  mzpsubst  26929  mzpresrename  26931  coeq0i  26935  eldioph2lem1  26942  lzunuz  26950  diophren  26999  pellexlem1  27017  pell14qrexpclnn0  27054  pellqrexplicit  27065  reglogcl  27078  reglogmul  27081  reglogexp  27082  rmxycomplete  27105  monotuz  27129  zindbi  27134  rmxypos  27137  jm2.17a  27150  congtr  27155  congmul  27157  congabseq  27164  acongsym  27166  acongrep  27170  fzneg  27172  acongeq  27173  dvdsabsmod0  27182  jm2.19  27189  jm2.20nn  27193  jm2.15nn0  27199  rmydioph  27210  rmxdiophlem  27211  jm3.1  27216  rpnnen3lem  27227  aomclem2  27255  islssfgi  27273  pwssplit4  27294  uvcval  27337  mapfien2  27361  lindsind2  27392  f1lindf  27395  lindsss  27397  f1linds  27398  lsslindf  27403  lsslinds  27404  islindf4  27411  lbslcic  27414  hbtlem1  27430  hbtlem2  27431  hbtlem5  27435  cnsrexpcl  27473  mndvcl  27549  mndvass  27550  mhmvlin  27555  hashgcdlem  27619  fmul01lt1lem1  27817  climsuselem1  27836  climsuse  27837  stoweidlem10  27862  stoweidlem14  27866  stoweidlem16  27868  stoweidlem17  27869  stoweidlem20  27872  stoweidlem34  27886  stoweidlem44  27896  stoweidlem57  27909  stoweidlem60  27912  wallispilem3  27919  f1oun2prg  28187  hashgt12el2  28219  nb3graprlem1  28287  nb3graprlem2  28288  nb3grapr  28289  cusgra2v  28297  cusgra3v  28299  iswlkon  28332  istrlon  28340  ispthon  28362  constr3lem4  28393  constr3trllem2  28397  constr3trllem5  28400  constr3pthlem2  28402  constr3cyclp  28408  3vfriswmgra  28429  n4cyclfrgra  28440  tratrb  28598  chordthmALT  29026  bnj240  29040  bnj836  29106  bnj545  29243  bnj600  29267  bnj966  29292  bnj967  29293  bnj1097  29327  bnj1118  29330  bnj1128  29336  bnj1204  29358  bnj1321  29373  bnj1408  29382  bnj1514  29409  lsmsat  29820  lcv1  29853  lub0N  30001  glb0N  30005  atcmp  30123  atnle  30129  cvlatcvr2  30154  hlsupr2  30198  cvrval3  30224  atcvr0eq  30237  2atlt  30250  llnnleat  30324  llnle  30329  llncmp  30333  2llnmat  30335  lplnle  30351  2lplnmN  30370  2llnmj  30371  lplncmp  30373  lvolcmp  30428  2lplnmj  30433  pmapmeet  30584  2lnat  30595  elpadd2at  30617  pclssN  30705  lhp0lt  30814  lhpj1  30833  lhpmcvr5N  30838  lhpmcvr6N  30839  ltrneq  30960  cdleme0aa  31021  cdleme10  31065  cdleme27a  31178  cdleme32fva  31248  cdleme42b  31289  cdlemf1  31372  cdlemg35  31524  tendovalco  31576  tendoidcl  31580  tendo0co2  31599  cdleml7  31793  dvhopvadd  31905  dvhopellsm  31929  dihmeetcN  32114  dihmeet  32155  mapdrvallem2  32457  mapdpglem32  32517
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