MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3ad2ant2 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  2938  vtoclgft  2962  vtoclegft  2983  epne3  4720  sofld  5277  funtpg  5460  fnprg  5464  fntpg  5465  fnco  5512  fvun1  5753  fsnunf2  5891  oprssov  6174  sorpssuni  6490  sorpssint  6491  onfununi  6562  onoviun  6564  smogt  6588  omass  6782  f1dom2g  7084  domunfican  7338  inelfi  7381  dffi2  7386  ordiso2  7440  wemapso  7476  unwdomg  7508  wdomima2g  7510  ixpiunwdom  7515  cantnfres  7589  dif1card  7848  ackbij1lem9  8064  ackbij1lem16  8071  cfflb  8095  coflim  8097  cfsmolem  8106  fincssdom  8159  isf32lem11  8199  domtriomlem  8278  axdc4lem  8291  ac6num  8315  axacndlem4  8441  axacndlem5  8442  axacnd  8443  elwina  8517  elina  8518  winaon  8519  inawina  8521  winacard  8523  winainflem  8524  tsksuc  8593  tskuni  8614  grupr  8628  nqereu  8762  enqeq  8767  nqereq  8768  adderpqlem  8787  mulerpqlem  8788  addassnq  8791  mulassnq  8792  distrnq  8794  ltsonq  8802  ltanq  8804  ltmnq  8805  div2neg  9693  lediv2  9856  nndivtr  9997  zdivmul  10298  gtndiv  10303  fzind  10324  eluzp1p1  10467  peano2uz  10486  xrre2  10714  xaddass  10784  xlt2add  10795  xmulasslem3  10821  xmulass  10822  supxrun  10850  icc0  10920  ubioc1  10921  ubicc2  10970  iccsplit  10985  elfzo0  11126  modabs  11229  modcyc  11231  moddi  11239  modsubdir  11240  expneg2  11345  expnbnd  11463  digit2  11467  hashnnn0genn0  11582  hashgadd  11606  hashinfxadd  11614  hashgt12el2  11638  hashfun  11655  brfi1indlem  11669  ccatval3  11702  ccatass  11705  swrd00  11720  swrdval2  11722  swrdlen  11725  ccatopth  11731  ccatopth2  11732  ccatco  11759  f1oun2prg  11819  swrds2  11835  rediv  11891  imdiv  11898  resqrex  12011  resqrcl  12014  limsupgle  12226  climuni  12301  mulcn2  12344  iseraltlem3  12432  rpnnen2lem7  12775  divalglem8  12875  ndvdssub  12882  bitsfzo  12902  mulgcd  13001  mulgcdr  13003  gcddiv  13004  rplpwr  13011  rppwr  13012  qredeq  13061  pythagtriplem1  13145  pythagtriplem3  13147  pythagtriplem10  13149  pythagtriplem6  13150  pythagtriplem7  13151  pythagtriplem11  13154  pythagtriplem12  13155  pythagtriplem13  13156  pythagtriplem14  13157  pythagtriplem16  13159  pythagtriplem19  13162  pythagtrip  13163  pcfaclem  13222  pcbc  13224  vdwapun  13297  vdwapid1  13298  imasaddvallem  13709  ismre  13770  mreincl  13779  submre  13785  mrcss  13796  comfeq  13887  cofurid  14043  xpcpropd  14260  issubmnd  14679  frmdup3  14766  cycsubg2cl  14933  ghmnsgima  14984  mndodcongi  15136  oddvdsnn0  15137  oddvds  15140  odeq  15143  odmulg2  15146  odmulg  15147  odhash2  15164  odhash3  15165  gexnnod  15177  gexcl2  15178  isslw  15197  subgslw  15205  oppglsm  15231  lsmsubm  15242  lsmless1  15248  lsmless2  15249  lsmass  15257  efgsval2  15320  efgsrel  15321  efgsfo  15326  ghmplusg  15416  odadd1  15418  odadd2  15419  gsumconst  15487  gsumsn  15498  ablfac1eu  15586  pgpfac1lem5  15592  ablfaclem3  15600  rngidss  15645  irredrmul  15767  abvres  15882  srngadd  15900  srngmul  15901  lssincl  15996  lsslsp  16046  reslmhm2b  16085  lsmsp  16113  sralmod  16213  aspid  16344  asclmul1  16353  asclmul2  16354  coe1add  16612  coe1addfv  16613  coe1subfv  16614  ntrin  17080  elnei  17130  restco  17182  restcldi  17191  sslm  17317  cnt1  17368  cmpsublem  17416  cmpcld  17419  kgen2ss  17540  upxp  17608  xkopjcn  17641  xkococnlem  17644  xkococn  17645  qtopval2  17681  qtoptop2  17684  ordthmeolem  17786  isfil2  17841  fgss  17858  fbasrn  17869  ufilmax  17892  filufint  17905  fmval  17928  elfm2  17933  elfm3  17935  rnelfmlem  17937  rnelfm  17938  flimrest  17968  flfnei  17976  isflf  17978  flffbas  17980  fclsrest  18009  cnpfcfi  18025  alexsubALTlem4  18034  subgntr  18089  opnsubg  18090  tgpconcompss  18096  divstgpopn  18102  divstgphaus  18105  utopsnnei  18232  blres  18414  metcnp3  18523  blval2  18558  xmsuspOLD  18568  xmsusp  18569  nmmtri  18621  nmrtri  18623  nminvr  18658  nmotri  18726  nghmplusg  18727  tgqioo  18784  iccpnfhmeo  18923  caun0  19187  cmetcusp1OLD  19258  cmetcusp1  19259  pjth  19293  volsup2  19450  itg2le  19584  dvn2bss  19769  evlsval2  19894  mdegldg  19942  mdegnn0cl  19947  deg1ldgdomn  19970  deg1mul3  19991  drnguc1p  20046  ig1peu  20047  ig1pdvds  20052  coeid3  20112  coe11  20124  dgradd2  20139  facth  20176  dvtaylp  20239  pserdvlem2  20297  ptolemy  20357  tanord1  20392  cxple2  20541  cxpeq  20594  isosctrlem2  20616  muval1  20869  dvdssqf  20874  chpwordi  20893  efchtdvds  20895  logfacbnd3  20960  bcmono  21014  efexple  21018  lgslem1  21033  lgsneg  21056  lgssq2  21073  lgsdirnn0  21076  dchrmusumlema  21140  selberglem3  21194  pntrmax  21211  padicabv  21277  usgra2edg  21355  fiusgraedgfi  21374  nbgraf1olem3  21406  nb3graprlem1  21413  nb3graprlem2  21414  nb3grapr  21415  cusgra2v  21424  cusgra3v  21426  cusgrasizeinds  21438  iswlkon  21484  istrlon  21494  ispthon  21529  isspthon  21536  constr1trl  21541  constr2spthlem1  21547  2pthlem2  21549  2wlklem1  21550  constr2pth  21554  2pthon  21555  constr3lem4  21587  constr3trllem2  21591  constr3trllem5  21594  constr3pthlem2  21596  constr3cyclp  21602  vdusgra0nedg  21632  gxmodid  21820  resgrprn  21821  ghomid  21906  nvsge0  22105  nmoub2i  22228  isblo3i  22255  dipassr2  22301  bcs2  22637  elspansn2  23022  fh2  23074  pjoi0  23172  homco2  23433  leopmul  23590  cdj3lem2  23891  rexdiv  24125  ofldadd  24191  ofldmul  24192  pstmfval  24244  unitdivcld  24252  nmmulg  24305  relogbcl  24355  sigaclcuni  24454  volss  24536  volfiniune  24539  dya2iocnrect  24584  sitmcl  24616  probun  24630  cndprobtot  24647  ballotlemsgt1  24721  ballotlemieq  24727  ballotlemfrcn0  24740  cnpcon  24870  cvmsf1o  24912  cvmscld  24913  cvmlift2lem6  24948  ghomfo  25055  modaddabs  25068  fzp1nel  25163  prodfn0  25175  prodfrec  25176  dfrdg2  25366  frrlem5e  25503  nobndlem8  25567  nofulllem2  25571  brbtwn2  25748  ax5seglem2  25772  ax5seglem3  25774  axlowdim  25804  axcontlem7  25813  axcontlem8  25814  fvtransport  25870  nndivsub  26111  mblfinlem  26143  itg2addnclem  26155  nn0prpwlem  26215  nn0prpw  26216  ivthALT  26228  fness  26252  topmeet  26283  fnejoin1  26287  f1ocan1fv  26318  f1ocan2fv  26319  upixp  26321  filbcmb  26332  mettrifi  26353  rngohom0  26478  rngohomsub  26479  rngokerinj  26481  intidl  26529  keridl  26532  nacsfix  26656  mapco2g  26659  mapfzcons  26662  mzpexpmpt  26692  mzpsubst  26695  mzpresrename  26697  coeq0i  26701  eldioph2lem1  26708  lzunuz  26716  diophren  26764  pellexlem1  26782  pell14qrexpclnn0  26819  pellqrexplicit  26830  reglogcl  26843  reglogmul  26846  reglogexp  26847  rmxycomplete  26870  monotuz  26894  zindbi  26899  rmxypos  26902  jm2.17a  26915  congtr  26920  congmul  26922  congabseq  26929  acongsym  26931  acongrep  26935  fzneg  26937  acongeq  26938  dvdsabsmod0  26947  jm2.19  26954  jm2.20nn  26958  jm2.15nn0  26964  rmydioph  26975  rmxdiophlem  26976  jm3.1  26981  rpnnen3lem  26992  aomclem2  27020  islssfgi  27038  pwssplit4  27059  uvcval  27102  mapfien2  27126  lindsind2  27157  f1lindf  27160  lindsss  27162  f1linds  27163  lsslindf  27168  lsslinds  27169  islindf4  27176  lbslcic  27179  hbtlem1  27195  hbtlem2  27196  hbtlem5  27200  cnsrexpcl  27238  mndvcl  27314  mndvass  27315  mhmvlin  27320  hashgcdlem  27384  fnchoice  27567  fmul01lt1lem1  27581  climsuselem1  27600  climsuse  27601  stoweidlem10  27626  stoweidlem14  27630  stoweidlem16  27632  stoweidlem17  27633  stoweidlem20  27636  stoweidlem44  27660  stoweidlem57  27673  stoweidlem60  27676  wallispilem3  27683  swrdnd  28001  addlenrevswrd  28004  swrd0swrd  28009  swrd0swrd0  28014  swrdccatin2  28018  swrdccatin12lem1  28019  swrdccatin12lem3a  28021  swrdccatin12lem3b  28022  swrdccatin12lem3c  28023  swrdccatin12lem3  28024  swrdccatin12lem4  28025  swrdccatin12  28026  swrdccatin12c  28028  swrdccat3  28029  swrdccat3a  28030  swrdccat3b  28031  usgra2pth  28041  el2wlkonot  28066  el2spthonot  28067  el2spthonot0  28068  el2wlkonotot0  28069  3vfriswmgra  28109  3cyclfrgrarn2  28118  n4cyclfrgra  28122  4cyclusnfrgra  28123  vdn0frgrav2  28128  vdn1frgrav2  28130  frg2woteqm  28162  frg2woteq  28163  2spot0  28167  usg2spot2nb  28168  frgregordn0  28173  tratrb  28331  chordthmALT  28755  bnj240  28769  bnj836  28835  bnj545  28972  bnj600  28996  bnj966  29021  bnj967  29022  bnj1097  29056  bnj1118  29059  bnj1128  29065  bnj1204  29087  bnj1321  29102  bnj1408  29111  bnj1514  29138  lsmsat  29491  lcv1  29524  lub0N  29672  glb0N  29676  atcmp  29794  atnle  29800  cvlatcvr2  29825  hlsupr2  29869  cvrval3  29895  atcvr0eq  29908  2atlt  29921  llnnleat  29995  llnle  30000  llncmp  30004  2llnmat  30006  lplnle  30022  2lplnmN  30041  2llnmj  30042  lplncmp  30044  lvolcmp  30099  2lplnmj  30104  pmapmeet  30255  2lnat  30266  elpadd2at  30288  pclssN  30376  lhp0lt  30485  lhpj1  30504  lhpmcvr5N  30509  lhpmcvr6N  30510  ltrneq  30631  cdleme0aa  30692  cdleme10  30736  cdleme27a  30849  cdleme32fva  30919  cdleme42b  30960  cdlemf1  31043  cdlemg35  31195  tendovalco  31247  tendoidcl  31251  tendo0co2  31270  cdleml7  31464  dvhopvadd  31576  dvhopellsm  31600  dihmeetcN  31785  dihmeet  31826  mapdrvallem2  32128  mapdpglem32  32188
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