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

Theorem adantld 467
Description: Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.)
Hypothesis
Ref Expression
adantld.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
adantld  |-  ( ph  ->  ( ( th  /\  ps )  ->  ch )
)

Proof of Theorem adantld
StepHypRef Expression
1 simpr 461 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adantld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 32 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  jaoa  510  dedlema  945  dedlemb  946  prlem1  953  2eu3  2374  unineq  3700  tz7.7  4845  ordsssuc2  4907  nnsuc  6595  poxp  6786  suppimacnv  6803  ressuppss  6810  imacosupp  6831  onnseq  6907  tz7.49  7002  oaass  7102  omordi  7107  nnmordi  7172  eroprf  7300  xpdom2  7508  inf3lem2  7938  trcl  8051  r1pwss  8094  cardaleph  8362  dfac2  8403  axcc4  8711  acncc  8712  zorn2lem7  8774  iundom2g  8807  cfpwsdom  8851  grothomex  9099  ltexprlem2  9309  1re  9488  00id  9647  mulge0  9960  uzindOLD  10839  xrlttr  11220  xmullem2  11331  snunioo  11514  fzen  11570  ssfzo12bi  11725  modirr  11872  hash2pr  12282  wrdlenfi  12362  cshweqrep  12559  limsupbnd2  13065  climrlim2  13129  climuni  13134  mulcn2  13177  serf0  13262  cvgcmp  13383  smuval2  13782  qnumdencl  13921  infpnlem1  14075  ram0  14187  prmlem1  14239  prmlem2  14251  catass  14728  sscfn1  14834  subccocl  14859  funcco  14885  gsmsymgrfixlem1  16036  psgnran  16125  efgi  16322  efgi2  16328  cntzcmnss  16431  dprddisj2  16644  dprddisj2OLD  16645  prmirredlem  18028  prmirredlemOLD  18031  psgnghm  18121  lmcls  19024  isfild  19549  flffbas  19686  cnpflf2  19691  divstgplem  19809  reperflem  20513  nmhmcn  20793  iscau2  20906  iscmet3lem2  20921  ivthlem2  21054  ovolmge0  21078  itg2seq  21338  limciun  21487  dveflem  21569  lhop1  21604  ftc1lem6  21631  mdegnn0cl  21660  aalioulem6  21921  pntlem3  22976  axlowdimlem16  23340  axcontlem12  23358  usgraedgprv  23432  usgrcyclnl2  23664  nvnencycllem  23666  iseupa  23723  ubthlem2  24409  shsvs  24863  mdsl2i  25863  mdsl2bi  25864  mdslmd1lem1  25866  atss  25887  chcv1  25896  chrelat2i  25906  atexch  25922  cdj3lem1  25975  bian1d  25988  disjxpin  26066  fpwrelmap  26169  nn0min  26226  sigaclci  26711  dya2iocuni  26834  subfacp1lem6  27209  ntrivcvg  27548  dfon2lem6  27737  dfrdg4  28117  altopth2  28133  cgrtriv  28169  cgrextend  28175  lineext  28243  btwnconn1  28268  colinbtwnle  28285  itg2addnc  28586  ftc1cnnc  28606  areacirclem1  28624  trer  28651  elicc3  28652  prnc  29007  ispridlc  29010  eldioph2b  29241  pell1234qrreccl  29335  islssfg2  29564  hbtlem2  29620  2reu3  30152  eluzgtdifelfzo  30359  hash3tr  30374  wlkv0  30431  usgra2wlkspthlem2  30437  2spontn0vne  30546  usg2spthonot0  30548  clwlkisclwwlklem2a4  30586  clwlkisclwwlklem1  30589  frgra3vlem1  30732  ztprmneprm  30879  pgrpgt2nabel  30911  telescfzgsum  30953  scmatscmids  31016  scmatmulcl  31042  snlindsntor  31114  cpmatacl  31181  fvmptnn04if  31305  sspwtrALT2  31861  bj-dfif5ALT  32388  bj-19.40b  32464  lcvexchlem4  32990  lcvexchlem5  32991  lkrss2N  33122  cvrnbtwn  33224  hlrelat2  33355  atle  33388  lvolex3N  33490  lplnnlelln  33495  llncvrlpln2  33509  lvolnlelln  33536  lvolnlelpln  33537  lplncvrlvol2  33567  snatpsubN  33702  linepsubN  33704  pmodlem2  33799  linepsubclN  33903  dihatexv  35291
  Copyright terms: Public domain W3C validator