Theorem adantll 476

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

Step	Hyp	Ref	Expression
1		simpr 110	. 2 |- ( ( th /\ ph ) -> ph )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan 283	1 |- ( ( ( th /\ ph ) /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ad2antlr  489  ad2ant2l  508  ad2ant2lr  510  ad5ant23  522  ad5ant24  523  ad5ant25  524  3ad2antl3  1188  3adant1l  1257  reu6  3009  sbc2iegf  3116  sbcralt  3122  sbcrext  3123  indifdir  3481  pofun  4438  poinxp  4824  ssimaex  5743  fndmdif  5788  dffo4  5830  fcompt  5852  fconst2g  5904  foco2  5932  foeqcnvco  5969  f1eqcocnv  5970  fliftel1  5973  isores3  5994  acexmid  6057  suppssdc  6473  tfrlemi14d  6577  tfrcl  6608  mapsnd  6936  dom2lem  7024  fiintim  7204  ordiso2  7339  mkvprop  7462  lt2addnq  7735  lt2mulnq  7736  ltexnqq  7739  genpdf  7839  addnqprl  7860  addnqpru  7861  addlocpr  7867  recexprlemopl  7956  caucvgsrlemgt1  8126  add4  8450  cnegex  8467  ltleadd  8737  zextle  9687  peano5uzti  9704  fnn0ind  9712  xrlttr  10147  xaddass  10221  iccshftr  10346  iccshftl  10348  iccdil  10350  icccntr  10352  fzaddel  10414  fzrev  10440  exbtwnzlemshrink  10632  xqltnle  10651  seq3val  10846  iseqf1olemab  10888  seqf1og  10907  exp3vallem  10926  mulexp  10964  expadd  10967  expmul  10970  leexp1a  10980  bccl  11154  hashfacen  11233  wrdnval  11280  swrdccat3blem  11456  ovshftex  11529  2shfti  11541  caucvgre  11691  cvg1nlemcau  11694  resqrexlemcvg  11729  cau3lem  11824  rexico  11931  iooinsup  11987  climmpt  12010  subcn2  12021  climrecvg1n  12058  climcvg1nlem  12059  climcaucn  12061  mertenslem2  12247  eftlcl  12399  reeftlcl  12400  dvdsext  12566  3dvds  12575  sqoddm1div8z  12597  bezoutlemaz  12724  bezoutr1  12754  dvdslcm  12791  lcmeq0  12793  lcmcl  12794  lcmneg  12796  lcmdvds  12801  coprmgcdb  12810  dvdsprime  12844  pc2dvds  13053  prmpwdvds  13078  infpnlem1  13082  1arith  13090  resmhm  13742  resmhm2b  13744  mhmco  13745  mhmima  13746  gsumwsubmcl  13751  dfgrp2  13782  mulgfng  13877  subgintm  13951  ghmmhmb  14007  resghm  14013  islmod  14565  islmodd  14567  cnco  15212  cnss1  15217  tx2cn  15261  upxp  15263  metss  15485  txmetcnp  15509  cncfss  15574  plyaddlem1  15738  plymullem1  15739  cosz12  15771  gausslemma2dlem4  16063  egrsubgr  16384  bj-findis  16875