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  2810  vtoclgft  2834  vtoclegft  2855  epne3  4572  sofld  5121  fnprg  5305  fnco  5352  fvun1  5590  fsnunf2  5719  oprssov  5989  sorpssuni  6286  sorpssint  6287  onfununi  6358  onoviun  6360  smogt  6384  omass  6578  f1dom2g  6879  domunfican  7129  dffi2  7176  ordiso2  7230  wemapso  7266  unwdomg  7298  wdomima2g  7300  ixpiunwdom  7305  cantnfres  7379  dif1card  7638  ackbij1lem9  7854  ackbij1lem16  7861  cfflb  7885  coflim  7887  cfsmolem  7896  fincssdom  7949  isf32lem11  7989  domtriomlem  8068  axdc4lem  8081  ac6num  8106  axacndlem4  8232  axacndlem5  8233  axacnd  8234  elwina  8308  elina  8309  winaon  8310  inawina  8312  winacard  8314  winainflem  8315  tsksuc  8384  tskuni  8405  grupr  8419  nqereu  8553  enqeq  8558  nqereq  8559  adderpqlem  8578  mulerpqlem  8579  addassnq  8582  mulassnq  8583  distrnq  8585  ltsonq  8593  ltanq  8595  ltmnq  8596  div2neg  9483  lediv2  9646  nndivtr  9787  zdivmul  10084  gtndiv  10089  fzind  10110  eluzp1p1  10253  peano2uz  10272  xrre2  10499  xaddass  10569  xlt2add  10580  xmulasslem3  10606  xmulass  10607  supxrun  10634  icc0  10704  ubioc1  10705  ubicc2  10753  iccsplit  10768  elfzo0  10904  modabs  10997  modcyc  10999  moddi  11007  modsubdir  11008  expneg2  11112  expnbnd  11230  digit2  11234  hashgadd  11359  hashfun  11389  ccatval3  11433  ccatass  11436  swrd00  11451  swrdval2  11453  swrdlen  11456  ccatopth  11462  ccatopth2  11463  ccatco  11490  swrds2  11560  rediv  11616  imdiv  11623  resqrex  11736  resqrcl  11739  limsupgle  11951  climuni  12026  mulcn2  12069  iseraltlem3  12156  rpnnen2lem7  12499  divalglem8  12599  ndvdssub  12606  bitsfzo  12626  mulgcd  12725  mulgcdr  12727  gcddiv  12728  rplpwr  12735  rppwr  12736  qredeq  12785  pythagtriplem1  12869  pythagtriplem3  12871  pythagtriplem10  12873  pythagtriplem6  12874  pythagtriplem7  12875  pythagtriplem11  12878  pythagtriplem12  12879  pythagtriplem13  12880  pythagtriplem14  12881  pythagtriplem16  12883  pythagtriplem19  12886  pythagtrip  12887  pcfaclem  12946  pcbc  12948  vdwapun  13021  vdwapid1  13022  imasaddvallem  13431  ismre  13492  mreincl  13501  submre  13507  mrcss  13518  comfeq  13609  cofurid  13765  xpcpropd  13982  issubmnd  14401  frmdup3  14488  cycsubg2cl  14655  ghmnsgima  14706  mndodcongi  14858  oddvdsnn0  14859  oddvds  14862  odeq  14865  odmulg2  14868  odmulg  14869  odhash2  14886  odhash3  14887  gexnnod  14899  gexcl2  14900  isslw  14919  subgslw  14927  oppglsm  14953  lsmsubm  14964  lsmless1  14970  lsmless2  14971  lsmass  14979  efgsval2  15042  efgsrel  15043  efgsfo  15048  ghmplusg  15138  odadd1  15140  odadd2  15141  gsumconst  15209  gsumsn  15220  ablfac1eu  15308  pgpfac1lem5  15314  ablfaclem3  15322  rngidss  15367  irredrmul  15489  abvres  15604  srngadd  15622  srngmul  15623  lssincl  15722  lsslsp  15772  reslmhm2b  15811  lsmsp  15839  sralmod  15939  aspid  16070  asclmul1  16079  asclmul2  16080  coe1add  16341  coe1addfv  16342  coe1subfv  16343  ntrin  16798  elnei  16848  restco  16895  restcldi  16904  sslm  17027  cnt1  17078  cmpsublem  17126  cmpcld  17129  kgen2ss  17250  upxp  17317  xkopjcn  17350  xkococnlem  17353  xkococn  17354  qtopval2  17387  qtoptop2  17390  ordthmeolem  17492  isfil2  17551  fgss  17568  fbasrn  17579  ufilmax  17602  filufint  17615  fmval  17638  elfm2  17643  elfm3  17645  rnelfmlem  17647  rnelfm  17648  flimrest  17678  flfnei  17686  isflf  17688  flffbas  17690  fclsrest  17719  cnpfcfi  17735  alexsubALTlem4  17744  subgntr  17789  opnsubg  17790  tgpconcompss  17796  divstgpopn  17802  divstgphaus  17805  blres  17977  metcnp3  18086  nmmtri  18143  nmrtri  18145  nminvr  18180  nmotri  18248  nghmplusg  18249  tgqioo  18306  iccpnfhmeo  18443  caun0  18707  pjth  18803  volsup2  18960  itg2le  19094  dvn2bss  19279  evlsval2  19404  mdegldg  19452  mdegnn0cl  19457  deg1ldgdomn  19480  deg1mul3  19501  drnguc1p  19556  ig1peu  19557  ig1pdvds  19562  coeid3  19622  coe11  19634  dgradd2  19649  facth  19686  dvtaylp  19749  pserdvlem2  19804  ptolemy  19864  tanord1  19899  cxple2  20044  cxpeq  20097  isosctrlem2  20119  muval1  20371  dvdssqf  20376  chpwordi  20395  efchtdvds  20397  logfacbnd3  20462  bcmono  20516  efexple  20520  lgslem1  20535  lgsneg  20558  lgssq2  20575  lgsdirnn0  20578  dchrmusumlema  20642  selberglem3  20696  pntrmax  20713  padicabv  20779  gxmodid  20946  resgrprn  20947  ghomid  21032  nvsge0  21229  nmoub2i  21352  isblo3i  21379  dipassr2  21425  bcs2  21761  elspansn2  22146  fh2  22198  pjoi0  22296  homco2  22557  leopmul  22714  cdj3lem2  23015  ballotlemsgt1  23069  ballotlemieq  23075  ballotlemfrcn0  23088  rexdiv  23109  unitdivcld  23285  relogbcl  23404  sigaclcuni  23479  probun  23622  cnpcon  23761  cvmsf1o  23803  cvmscld  23804  cvmlift2lem6  23839  ghomfo  23998  modaddabs  24011  dfrdg2  24152  frrlem5e  24289  nobndlem8  24353  nofulllem2  24357  brbtwn2  24533  ax5seglem2  24557  ax5seglem3  24559  axlowdim  24589  axcontlem7  24598  axcontlem8  24599  fvtransport  24655  nndivsub  24896  iccss3  25134  injsurinj  25149  valcurfn1  25204  int2pre  25237  supwval  25284  dfps2  25289  clfsebsr  25349  fprodadd  25352  fprodneg  25378  fprodsub  25379  prsubrtr  25399  mulveczer  25479  mulinvsca  25480  svli2  25484  svs2  25487  truni1  25505  truni3  25507  intfmu2  25519  npmp  25521  cmptdst  25568  prdnei  25573  islimrs4  25582  mslb1  25607  2wsms  25608  lvsovso  25626  supnufb  25630  claddrv  25647  claddrvr  25648  addassv  25656  negveud  25668  negveudr  25669  issubrv  25672  idosd  25744  dmrngcmp  25751  1cat  25759  imonclem  25813  cmpmon  25815  icmpmon  25816  idmon  25817  isepic  25824  morsubc  25855  vtarl  25887  tartarmap  25888  fnctartar2  25908  codcatfun  25934  cmp2morpcats  25961  cmppar3  25974  isconc3  26008  clscnc  26010  isconcl5ab  26102  bsstrs  26146  nbssntrs  26147  bosser  26167  pdiveql  26168  isibcg  26191  nn0prpwlem  26238  nn0prpw  26239  ivthALT  26258  fness  26282  topmeet  26313  fnejoin1  26317  f1ocan1fv  26394  f1ocan2fv  26395  upixp  26403  filbcmb  26432  mettrifi  26473  rngohom0  26603  rngohomsub  26604  rngokerinj  26606  intidl  26654  keridl  26657  nacsfix  26787  mapco2g  26790  mapfzcons  26793  mzpexpmpt  26823  mzpsubst  26826  mzpresrename  26828  coeq0i  26832  eldioph2lem1  26839  lzunuz  26847  diophren  26896  pellexlem1  26914  pell14qrexpclnn0  26951  pellqrexplicit  26962  reglogcl  26975  reglogmul  26978  reglogexp  26979  rmxycomplete  27002  monotuz  27026  zindbi  27031  rmxypos  27034  jm2.17a  27047  congtr  27052  congmul  27054  congabseq  27061  acongsym  27063  acongrep  27067  fzneg  27069  acongeq  27070  dvdsabsmod0  27079  jm2.19  27086  jm2.20nn  27090  jm2.15nn0  27096  rmydioph  27107  rmxdiophlem  27108  jm3.1  27113  rpnnen3lem  27124  aomclem2  27152  islssfgi  27170  pwssplit4  27191  uvcval  27234  mapfien2  27258  lindsind2  27289  f1lindf  27292  lindsss  27294  f1linds  27295  lsslindf  27300  lsslinds  27301  islindf4  27308  lbslcic  27311  hbtlem1  27327  hbtlem2  27328  hbtlem5  27332  cnsrexpcl  27370  mndvcl  27446  mndvass  27447  mhmvlin  27452  hashgcdlem  27516  fmul01lt1lem1  27714  climsuselem1  27733  climsuse  27734  stoweidlem10  27759  stoweidlem14  27763  stoweidlem16  27765  stoweidlem17  27766  stoweidlem20  27769  stoweidlem34  27783  stoweidlem44  27793  stoweidlem57  27806  stoweidlem60  27809  wallispilem3  27816  f1oun2prg  28076  cusgra2v  28158  3vfriswmgra  28183  tratrb  28299  chordthmALT  28710  bnj240  28724  bnj836  28790  bnj545  28927  bnj600  28951  bnj966  28976  bnj967  28977  bnj1097  29011  bnj1118  29014  bnj1128  29020  bnj1204  29042  bnj1321  29057  bnj1408  29066  bnj1514  29093  lsmsat  29198  lcv1  29231  lub0N  29379  glb0N  29383  atcmp  29501  atnle  29507  cvlatcvr2  29532  hlsupr2  29576  cvrval3  29602  atcvr0eq  29615  2atlt  29628  llnnleat  29702  llnle  29707  llncmp  29711  2llnmat  29713  lplnle  29729  2lplnmN  29748  2llnmj  29749  lplncmp  29751  lvolcmp  29806  2lplnmj  29811  pmapmeet  29962  2lnat  29973  elpadd2at  29995  pclssN  30083  lhp0lt  30192  lhpj1  30211  lhpmcvr5N  30216  lhpmcvr6N  30217  ltrneq  30338  cdleme0aa  30399  cdleme10  30443  cdleme27a  30556  cdleme32fva  30626  cdleme42b  30667  cdlemf1  30750  cdlemg35  30902  tendovalco  30954  tendoidcl  30958  tendo0co2  30977  cdleml7  31171  dvhopvadd  31283  dvhopellsm  31307  dihmeetcN  31492  dihmeet  31533  mapdrvallem2  31835  mapdpglem32  31895
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