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

Theorem 3ad2ant2 979
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 452 . 2  |-  ( (
ph  /\  th )  ->  ch )
323adant1 975 1  |-  ( ( ps  /\  ph  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simp2l  983  simp2r  984  simp21  990  simp22  991  simp23  992  simp2ll  1024  simp2lr  1025  simp2rl  1026  simp2rr  1027  simp2l1  1056  simp2l2  1057  simp2l3  1058  simp2r1  1059  simp2r2  1060  simp2r3  1061  simp21l  1074  simp21r  1075  simp22l  1076  simp22r  1077  simp23l  1078  simp23r  1079  simp211  1095  simp212  1096  simp213  1097  simp221  1098  simp222  1099  simp223  1100  simp231  1101  simp232  1102  simp233  1103  3anim123i  1139  3jaao  1251  ceqsalt  2970  vtoclgft  2994  vtoclegft  3015  epne3  4753  sofld  5310  funtpg  5493  fnprg  5497  fntpg  5498  fnco  5545  fvun1  5786  fsnunf2  5924  oprssov  6207  sorpssuni  6523  sorpssint  6524  onfununi  6595  onoviun  6597  smogt  6621  omass  6815  f1dom2g  7117  domunfican  7371  inelfi  7415  dffi2  7420  ordiso2  7476  wemapso  7512  unwdomg  7544  wdomima2g  7546  ixpiunwdom  7551  cantnfres  7625  dif1card  7884  ackbij1lem9  8100  ackbij1lem16  8107  cfflb  8131  coflim  8133  cfsmolem  8142  fincssdom  8195  isf32lem11  8235  domtriomlem  8314  axdc4lem  8327  ac6num  8351  axacndlem4  8477  axacndlem5  8478  axacnd  8479  elwina  8553  elina  8554  winaon  8555  inawina  8557  winacard  8559  winainflem  8560  tsksuc  8629  tskuni  8650  grupr  8664  nqereu  8798  enqeq  8803  nqereq  8804  adderpqlem  8823  mulerpqlem  8824  addassnq  8827  mulassnq  8828  distrnq  8830  ltsonq  8838  ltanq  8840  ltmnq  8841  div2neg  9729  lediv2  9892  nndivtr  10033  zdivmul  10334  gtndiv  10339  fzind  10360  eluzp1p1  10503  peano2uz  10522  xrre2  10750  xaddass  10820  xlt2add  10831  xmulasslem3  10857  xmulass  10858  supxrun  10886  icc0  10956  ubioc1  10957  ubicc2  11006  iccsplit  11021  elfzo0  11163  modabs  11266  modcyc  11268  moddi  11276  modsubdir  11277  expneg2  11382  expnbnd  11500  digit2  11504  hashnnn0genn0  11619  hashgadd  11643  hashinfxadd  11651  hashgt12el2  11675  hashfun  11692  brfi1indlem  11706  ccatval3  11739  ccatass  11742  swrd00  11757  swrdval2  11759  swrdlen  11762  ccatopth  11768  ccatopth2  11769  ccatco  11796  f1oun2prg  11856  swrds2  11872  rediv  11928  imdiv  11935  resqrex  12048  resqrcl  12051  limsupgle  12263  climuni  12338  mulcn2  12381  iseraltlem3  12469  rpnnen2lem7  12812  divalglem8  12912  ndvdssub  12919  bitsfzo  12939  mulgcd  13038  mulgcdr  13040  gcddiv  13041  rplpwr  13048  rppwr  13049  qredeq  13098  pythagtriplem1  13182  pythagtriplem3  13184  pythagtriplem10  13186  pythagtriplem6  13187  pythagtriplem7  13188  pythagtriplem11  13191  pythagtriplem12  13192  pythagtriplem13  13193  pythagtriplem14  13194  pythagtriplem16  13196  pythagtriplem19  13199  pythagtrip  13200  pcfaclem  13259  pcbc  13261  vdwapun  13334  vdwapid1  13335  imasaddvallem  13746  ismre  13807  mreincl  13816  submre  13822  mrcss  13833  comfeq  13924  cofurid  14080  xpcpropd  14297  issubmnd  14716  frmdup3  14803  cycsubg2cl  14970  ghmnsgima  15021  mndodcongi  15173  oddvdsnn0  15174  oddvds  15177  odeq  15180  odmulg2  15183  odmulg  15184  odhash2  15201  odhash3  15202  gexnnod  15214  gexcl2  15215  isslw  15234  subgslw  15242  oppglsm  15268  lsmsubm  15279  lsmless1  15285  lsmless2  15286  lsmass  15294  efgsval2  15357  efgsrel  15358  efgsfo  15363  ghmplusg  15453  odadd1  15455  odadd2  15456  gsumconst  15524  gsumsn  15535  ablfac1eu  15623  pgpfac1lem5  15629  ablfaclem3  15637  rngidss  15682  irredrmul  15804  abvres  15919  srngadd  15937  srngmul  15938  lssincl  16033  lsslsp  16083  reslmhm2b  16122  lsmsp  16150  sralmod  16250  aspid  16381  asclmul1  16390  asclmul2  16391  coe1add  16649  coe1addfv  16650  coe1subfv  16651  ntrin  17117  elnei  17167  restco  17220  restcldi  17229  sslm  17355  cnt1  17406  cmpsublem  17454  cmpcld  17457  kgen2ss  17579  upxp  17647  xkopjcn  17680  xkococnlem  17683  xkococn  17684  qtopval2  17720  qtoptop2  17723  ordthmeolem  17825  isfil2  17880  fgss  17897  fbasrn  17908  ufilmax  17931  filufint  17944  fmval  17967  elfm2  17972  elfm3  17974  rnelfmlem  17976  rnelfm  17977  flimrest  18007  flfnei  18015  isflf  18017  flffbas  18019  fclsrest  18048  cnpfcfi  18064  alexsubALTlem4  18073  subgntr  18128  opnsubg  18129  tgpconcompss  18135  divstgpopn  18141  divstgphaus  18144  utopsnnei  18271  blres  18453  metcnp3  18562  blval2  18597  xmsuspOLD  18607  xmsusp  18608  nmmtri  18660  nmrtri  18662  nminvr  18697  nmotri  18765  nghmplusg  18766  tgqioo  18823  iccpnfhmeo  18962  caun0  19226  cmetcusp1OLD  19297  cmetcusp1  19298  pjth  19332  volsup2  19489  itg2le  19623  dvn2bss  19808  evlsval2  19933  mdegldg  19981  mdegnn0cl  19986  deg1ldgdomn  20009  deg1mul3  20030  drnguc1p  20085  ig1peu  20086  ig1pdvds  20091  coeid3  20151  coe11  20163  dgradd2  20178  facth  20215  dvtaylp  20278  pserdvlem2  20336  ptolemy  20396  tanord1  20431  cxple2  20580  cxpeq  20633  isosctrlem2  20655  muval1  20908  dvdssqf  20913  chpwordi  20932  efchtdvds  20934  logfacbnd3  20999  bcmono  21053  efexple  21057  lgslem1  21072  lgsneg  21095  lgssq2  21112  lgsdirnn0  21115  dchrmusumlema  21179  selberglem3  21233  pntrmax  21250  padicabv  21316  usgra2edg  21394  fiusgraedgfi  21413  nbgraf1olem3  21445  nb3graprlem1  21452  nb3graprlem2  21453  nb3grapr  21454  cusgra2v  21463  cusgra3v  21465  cusgrasizeinds  21477  iswlkon  21523  istrlon  21533  ispthon  21568  isspthon  21575  constr1trl  21580  constr2spthlem1  21586  2pthlem2  21588  2wlklem1  21589  constr2pth  21593  2pthon  21594  constr3lem4  21626  constr3trllem2  21630  constr3trllem5  21633  constr3pthlem2  21635  constr3cyclp  21641  vdusgra0nedg  21671  gxmodid  21859  resgrprn  21860  ghomid  21945  nvsge0  22144  nmoub2i  22267  isblo3i  22294  dipassr2  22340  bcs2  22676  elspansn2  23061  fh2  23113  pjoi0  23211  homco2  23472  leopmul  23629  cdj3lem2  23930  rexdiv  24164  ofldadd  24230  ofldmul  24231  pstmfval  24283  unitdivcld  24291  nmmulg  24344  relogbcl  24394  sigaclcuni  24493  volss  24575  volfiniune  24578  dya2iocnrect  24623  sitmcl  24655  probun  24669  cndprobtot  24686  ballotlemsgt1  24760  ballotlemieq  24766  ballotlemfrcn0  24779  cnpcon  24909  cvmsf1o  24951  cvmscld  24952  cvmlift2lem6  24987  ghomfo  25094  modaddabs  25107  fzp1nel  25202  prodfn0  25214  prodfrec  25215  dfrdg2  25415  wrecseq123  25524  frrlem5e  25582  nobndlem8  25646  nofulllem2  25650  brbtwn2  25836  ax5seglem2  25860  ax5seglem3  25862  axlowdim  25892  axcontlem7  25901  axcontlem8  25902  fvtransport  25958  nndivsub  26199  mblfinlem  26234  itg2addnclem  26246  nn0prpwlem  26316  nn0prpw  26317  ivthALT  26329  fness  26353  topmeet  26384  fnejoin1  26388  f1ocan1fv  26419  f1ocan2fv  26420  upixp  26422  filbcmb  26433  mettrifi  26454  rngohom0  26579  rngohomsub  26580  rngokerinj  26582  intidl  26630  keridl  26633  nacsfix  26757  mapco2g  26760  mapfzcons  26763  mzpexpmpt  26793  mzpsubst  26796  mzpresrename  26798  coeq0i  26802  eldioph2lem1  26809  lzunuz  26817  diophren  26865  pellexlem1  26883  pell14qrexpclnn0  26920  pellqrexplicit  26931  reglogcl  26944  reglogmul  26947  reglogexp  26948  rmxycomplete  26971  monotuz  26995  zindbi  27000  rmxypos  27003  jm2.17a  27016  congtr  27021  congmul  27023  congabseq  27030  acongsym  27032  acongrep  27036  fzneg  27038  acongeq  27039  dvdsabsmod0  27048  jm2.19  27055  jm2.20nn  27059  jm2.15nn0  27065  rmydioph  27076  rmxdiophlem  27077  jm3.1  27082  rpnnen3lem  27093  aomclem2  27121  islssfgi  27138  pwssplit4  27159  uvcval  27202  mapfien2  27226  lindsind2  27257  f1lindf  27260  lindsss  27262  f1linds  27263  lsslindf  27268  lsslinds  27269  islindf4  27276  lbslcic  27279  hbtlem1  27295  hbtlem2  27296  hbtlem5  27300  cnsrexpcl  27338  mndvcl  27414  mndvass  27415  mhmvlin  27420  hashgcdlem  27484  fnchoice  27667  fmul01lt1lem1  27681  climsuselem1  27700  climsuse  27701  stoweidlem10  27726  stoweidlem14  27730  stoweidlem16  27732  stoweidlem17  27733  stoweidlem20  27736  stoweidlem44  27760  stoweidlem57  27773  stoweidlem60  27776  wallispilem3  27783  fz0fzdiffz0  28103  subsubelfzo0  28118  ltdifltdiv  28126  modadd2mod  28132  swrdnd  28154  addlenrevswrd  28157  swrdvalodm2  28160  swrd0swrd  28163  swrd0swrd0  28168  swrdccatin12lem4  28179  swrdccat3  28181  swrdccat  28182  swrdccat3a  28183  swrdccat3b  28185  modprm0  28194  cshwidx  28208  cshwidxmod  28209  2cshw1lem1  28214  2cshw1  28217  2cshw2lem1  28218  2cshw2lem2  28219  2cshw2  28221  cshweqdif2  28233  cshweqdif2s  28234  cshwssizelem2  28244  cshwssizelem4a  28246  usgra2pth  28264  el2wlkonot  28289  el2spthonot  28290  el2spthonot0  28291  el2wlkonotot0  28292  3vfriswmgra  28332  3cyclfrgrarn2  28341  n4cyclfrgra  28345  4cyclusnfrgra  28346  vdn0frgrav2  28351  vdn1frgrav2  28353  frg2woteqm  28385  frg2woteq  28386  2spot0  28390  usg2spot2nb  28391  frgregordn0  28396  tratrb  28557  chordthmALT  28982  bnj240  29000  bnj836  29066  bnj545  29203  bnj600  29227  bnj966  29252  bnj967  29253  bnj1097  29287  bnj1118  29290  bnj1128  29296  bnj1204  29318  bnj1321  29333  bnj1408  29342  bnj1514  29369  lsmsat  29743  lcv1  29776  lub0N  29924  glb0N  29928  atcmp  30046  atnle  30052  cvlatcvr2  30077  hlsupr2  30121  cvrval3  30147  atcvr0eq  30160  2atlt  30173  llnnleat  30247  llnle  30252  llncmp  30256  2llnmat  30258  lplnle  30274  2lplnmN  30293  2llnmj  30294  lplncmp  30296  lvolcmp  30351  2lplnmj  30356  pmapmeet  30507  2lnat  30518  elpadd2at  30540  pclssN  30628  lhp0lt  30737  lhpj1  30756  lhpmcvr5N  30761  lhpmcvr6N  30762  ltrneq  30883  cdleme0aa  30944  cdleme10  30988  cdleme27a  31101  cdleme32fva  31171  cdleme42b  31212  cdlemf1  31295  cdlemg35  31447  tendovalco  31499  tendoidcl  31503  tendo0co2  31522  cdleml7  31716  dvhopvadd  31828  dvhopellsm  31852  dihmeetcN  32037  dihmeet  32078  mapdrvallem2  32380  mapdpglem32  32440
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