Theorem adantll 459

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 108	. 2 |- ( ( th /\ ph ) -> ph )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan 277	1 |- ( ( ( th /\ ph ) /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  ad2antlr  472  ad2ant2l  491  ad2ant2lr  493  3ad2antl3  1102  3adant1l  1161  reu6  2781  sbc2iegf  2884  sbcralt  2890  sbcrext  2891  indifdir  3220  pofun  4067  poinxp  4427  ssimaex  5255  fndmdif  5293  dffo4  5336  foco2  5339  fcompt  5354  fconst2g  5397  foeqcnvco  5450  f1eqcocnv  5451  fliftel1  5454  isores3  5475  acexmid  5531  tfrlemi14d  5970  dom2lem  6275  ordiso2  6446  lt2addnq  6594  lt2mulnq  6595  ltexnqq  6598  genpdf  6698  addnqprl  6719  addnqpru  6720  addlocpr  6726  recexprlemopl  6815  caucvgsrlemgt1  6971  add4  7269  cnegex  7286  ltleadd  7550  zextle  8438  peano5uzti  8455  fnn0ind  8463  xrlttr  8870  iccshftr  9016  iccshftl  9018  iccdil  9020  icccntr  9022  fzaddel  9077  fzrev  9101  expivallem  9477  expival  9478  mulexp  9515  expadd  9518  expmul  9521  leexp1a  9531  bccl  9694  ovshftex  9707  2shfti  9719  caucvgre  9867  cvg1nlemcau  9870  resqrexlemcvg  9905  cau3lem  10000  rexico  10107  climmpt  10139  subcn2  10150  climrecvg1n  10185  climcvg1nlem  10186  climcaucn  10188  dvdsext  10255  sqoddm1div8z  10286  bezoutlemaz  10392  bezoutr1  10422  dvdslcm  10451  lcmeq0  10453  lcmcl  10454  lcmneg  10456  lcmdvds  10461  coprmgcdb  10470  dvdsprime  10504  bj-findis  10774