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

Theorem adantll 694
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
adant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
adantll  |-  ( ( ( th  /\  ph )  /\  ps )  ->  ch )

Proof of Theorem adantll
StepHypRef Expression
1 simpr 447 . 2  |-  ( ( th  /\  ph )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 457 1  |-  ( ( ( th  /\  ph )  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  ad2antlr  707  ad2ant2l  726  ad2ant2lr  728  3ad2antl3  1119  3adant1l  1174  ax11eq  2134  ax11el  2135  nfeud2  2157  ralcom2  2706  reu6  2956  sbc2iegf  3059  sbcralt  3065  pofun  4332  tz7.7  4420  onfr  4433  limsssuc  4643  poinxp  4755  sossfld  5122  ssimaex  5586  fndmdif  5631  dffo4  5678  foco2  5682  fcompt  5696  fconst2g  5730  isores3  5834  curry1  6212  curry2  6215  onnseq  6363  oe0  6523  oesuclem  6526  oecl  6538  oaordi  6546  oawordri  6550  oaass  6561  omordi  6566  omword2  6574  omlimcl  6578  odi  6579  omass  6580  oeoe  6599  nnaordi  6618  oaabs  6644  omsmolem  6653  eceqoveq  6765  dom2lem  6903  sbthlem9  6981  php3  7049  onomeneq  7052  isinf  7078  frfi  7104  fiint  7135  fodomfib  7138  fofinf1o  7139  marypha1lem  7188  ordiso2  7232  unwdomg  7300  xpwdomg  7301  ac5num  7665  cff1  7886  cfcoflem  7900  infpssrlem4  7934  isf32lem9  7989  isf34lem7  8007  fin1a2lem13  8040  fin1a2s  8042  hsmexlem4  8057  axdc2lem  8076  zorn2lem6  8130  inttsk  8398  tskuni  8407  nqereu  8555  prcdnq  8619  addclprlem2  8643  ltexpri  8669  prlem936  8673  reclem2pr  8674  axsup  8900  add4  9029  ltleadd  9259  lt2mul2div  9634  lediv12a  9651  infmrcl  9735  nn2ge  9773  zextle  10087  fnn0ind  10113  xrlttr  10476  ifle  10526  xaddass  10571  xmulasslem3  10608  xlemul1a  10610  xadddilem  10616  xrsupsslem  10627  xrinfmsslem  10628  supxrunb1  10640  supxrunb2  10641  ixxin  10675  difreicc  10769  iccsplit  10770  iccshftr  10771  iccshftl  10773  iccdil  10775  icccntr  10777  fzaddel  10828  fzrev  10848  modadd1  11003  modmul1  11004  mulexp  11143  expadd  11146  expmul  11149  leexp1a  11162  expnbnd  11232  bccl  11336  hashdom  11363  hashfacen  11394  revccat  11486  2shfti  11577  cau3lem  11840  subcn2  12070  caucvgb  12154  iseraltlem1  12156  sumss  12199  incexclem  12297  supcvg  12316  mertenslem2  12343  eftlcl  12389  reeftlcl  12390  rpnnen2lem6  12500  dvdsext  12581  3dvds  12593  gcdcllem3  12694  seq1st  12743  dvdsprime  12773  pc2dvds  12933  prmpwdvds  12953  unbenlem  12957  infpnlem1  12959  1arith  12976  vdwmc2  13028  ramcl  13078  mrcuni  13525  isacs1i  13561  acsfn  13563  funcpropd  13776  natpropd  13852  curfcl  14008  curf2ndf  14023  spwpr2  14339  resmhm  14438  resmhm2b  14440  mhmco  14441  mhmima  14442  pwsdiagmhm  14447  gsumwsubmcl  14463  gsumwspan  14470  subgint  14643  ghmmhmb  14696  resghm  14701  cntzmhm  14816  dfod2  14879  gexdvds  14897  subgpgp  14910  sylow1lem3  14913  frgpnabllem1  15163  dprdfeq0  15259  isdrng2  15524  cntzsubr  15579  islmodd  15635  lsslss  15720  reslmhm2b  15813  psrbaglefi  16120  ply1coe  16370  ocvocv  16573  elcls  16812  leordtval  16945  cnpnei  16995  cnco  16997  cnss1  17007  cmpsub  17129  hauscmplem  17135  ptbasid  17272  tx2cn  17306  upxp  17319  txindis  17330  xkoptsub  17350  xkopt  17351  trfbas2  17540  filcon  17580  trfil2  17584  filssufilg  17608  ufileu  17616  fixufil  17619  ufilen  17627  rnelfmlem  17649  flimclsi  17675  hauspwpwf1  17684  fclsopn  17711  fclsfnflim  17724  fclscmpi  17726  alexsubALTlem3  17745  alexsubALTlem4  17746  ptcmplem5  17752  tgpmulg  17778  subgtgp  17790  tgpt0  17803  tsmsxplem2  17838  metss  18056  dscopn  18098  xrsmopn  18320  cncfss  18405  icoopnst  18439  iccpnfcnv  18444  icccvx  18450  evth  18459  phtpycc  18491  pcohtpylem  18519  lmmbrf  18690  fgcfil  18699  caucfil  18711  cfilres  18724  bcth3  18755  ovolfioo  18829  ovolficc  18830  voliunlem3  18911  volcn  18963  mbflimsup  19023  mbfi1fseqlem5  19076  itg2seq  19099  dvnff  19274  dvnadd  19280  cpnord  19286  c1liplem1  19345  plypf1  19596  plyaddlem1  19597  plymullem1  19598  coeeulem  19608  coeidlem  19621  dgrle  19627  plycjlem  19659  elqaalem3  19703  ulmcaulem  19773  ulmcau  19774  psergf  19790  psercn2  19801  efopn  20007  abscxpbnd  20095  leibpi  20240  isppw2  20355  muinv  20435  bposlem3  20527  pntrmax  20715  pntpbnd1  20737  qabvexp  20777  grpoidinvlem3  20875  grpoidinv  20877  grpoideu  20878  subgoablo  20980  nmoub3i  21353  nmlno0lem  21373  nmlnoubi  21376  ipasslem3  21413  ipblnfi  21436  hvaddsub4  21659  his35  21669  shsel3  21896  chj4  22116  spansncol  22149  chscllem2  22219  5oalem2  22236  3oalem2  22244  hoaddcl  22340  adjsym  22415  cnvadj  22474  hhcno  22486  hhcnf  22487  nmopub2tALT  22491  unoplin  22502  counop  22503  nmfnleub2  22508  hmoplin  22524  brafnmul  22533  nmlnop0iALT  22577  nmopun  22596  nmophmi  22613  riesz3i  22644  riesz1  22647  cnlnadjlem2  22650  cnlnadjlem6  22654  adjmul  22674  adjadd  22675  bra11  22690  cnvbraval  22692  kbass5  22702  kbass6  22703  leop2  22706  leopadd  22714  leopmuli  22715  leoptri  22718  leopnmid  22720  nmopleid  22721  pj3si  22789  hstel2  22801  cvcon3  22866  dmdmd  22882  dmdbr5  22890  mdsl0  22892  mdslmd1lem1  22907  mdslmd1lem2  22908  mdslmd3i  22914  superpos  22936  chirredlem2  22973  chirredlem3  22974  mdsymlem3  22987  mdsymlem5  22989  mdsymlem6  22990  sumdmdlem  23000  cdjreui  23014  cdj1i  23015  cdj3i  23023  fcomptf  23232  xrge0iifcnv  23317  hasheuni  23455  sigaclcu2  23483  insiga  23500  sconpi1  23772  cvmsss2  23807  eupath2lem3  23905  dfon2lem6  24146  predpo  24186  preddowncl  24198  dftrpred3g  24238  poseq  24255  soseq  24256  nodenselem3  24339  nobndlem6  24353  eqeelen  24534  colinearalglem4  24539  axcgrid  24546  axsegconlem1  24547  axsegconlem3  24549  ax5seglem1  24558  ax5seglem2  24559  ax5seglem9  24567  axcontlem2  24595  hfext  24815  itg2addnclem2  24934  itg2addnc  24935  surjsec2  25131  toplat  25301  ltrcmp  25416  supexr  25642  idsubfun  25869  elicc3  26239  fnessref  26304  eqfnun  26398  indexdom  26424  filbcmb  26443  fzadd2  26455  fdc  26466  incsequz  26469  metf1o  26480  caures  26487  bndss  26521  ismtycnv  26537  heiborlem1  26546  rrncmslem  26567  isdrngo2  26600  rngoisocnv  26623  unichnidl  26667  nacsfix  26798  eq0rabdioph  26867  diophren  26907  rencldnfilem  26914  pell1234qrdich  26957  jm2.24  27061  bezoutr1  27084  jm2.26lem3  27105  wepwsolem  27149  pwssplit4  27202  frlmsslsp  27259  frlmlbs  27260  isnumbasgrplem3  27281  dgrnznn  27351  f1omvdconj  27400  mamudi  27472  mamudir  27473  ofsubid  27552  stirlinglem5  27838  lshpset2N  29382  pmapglb2N  30033  pmapglb2xN  30034  pclfinN  30162  polval2N  30168  cdleme31fv2  30655  cdleme32fvcl  30702  cdleme48gfv  30799  tendoicl  31058  tendoipl  31059  diaglbN  31318  dochkr1  31741  dochkr1OLDN  31742
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
  Copyright terms: Public domain W3C validator