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  3006  sbc2iegf  3113  sbcralt  3119  sbcrext  3120  indifdir  3477  pofun  4433  poinxp  4819  ssimaex  5738  fndmdif  5783  dffo4  5825  fcompt  5847  fconst2g  5899  foco2  5926  foeqcnvco  5963  f1eqcocnv  5964  fliftel1  5967  isores3  5988  acexmid  6049  suppssdc  6460  tfrlemi14d  6564  tfrcl  6595  mapsnd  6923  dom2lem  7011  fiintim  7191  ordiso2  7326  mkvprop  7449  lt2addnq  7719  lt2mulnq  7720  ltexnqq  7723  genpdf  7823  addnqprl  7844  addnqpru  7845  addlocpr  7851  recexprlemopl  7940  caucvgsrlemgt1  8110  add4  8434  cnegex  8451  ltleadd  8720  zextle  9669  peano5uzti  9686  fnn0ind  9694  xrlttr  10128  xaddass  10202  iccshftr  10327  iccshftl  10329  iccdil  10331  icccntr  10333  fzaddel  10393  fzrev  10418  exbtwnzlemshrink  10608  xqltnle  10627  seq3val  10822  iseqf1olemab  10864  seqf1og  10883  exp3vallem  10902  mulexp  10940  expadd  10943  expmul  10946  leexp1a  10956  bccl  11129  hashfacen  11208  wrdnval  11255  swrdccat3blem  11431  ovshftex  11504  2shfti  11516  caucvgre  11666  cvg1nlemcau  11669  resqrexlemcvg  11704  cau3lem  11799  rexico  11906  iooinsup  11962  climmpt  11985  subcn2  11996  climrecvg1n  12033  climcvg1nlem  12034  climcaucn  12036  mertenslem2  12222  eftlcl  12374  reeftlcl  12375  dvdsext  12541  3dvds  12550  sqoddm1div8z  12572  bezoutlemaz  12699  bezoutr1  12729  dvdslcm  12766  lcmeq0  12768  lcmcl  12769  lcmneg  12771  lcmdvds  12776  coprmgcdb  12785  dvdsprime  12819  pc2dvds  13028  prmpwdvds  13053  infpnlem1  13057  1arith  13065  resmhm  13700  resmhm2b  13702  mhmco  13703  mhmima  13704  gsumwsubmcl  13709  dfgrp2  13740  mulgfng  13841  subgintm  13915  ghmmhmb  13971  resghm  13977  islmod  14439  islmodd  14441  cnco  15086  cnss1  15091  tx2cn  15135  upxp  15137  metss  15359  txmetcnp  15383  cncfss  15448  plyaddlem1  15612  plymullem1  15613  cosz12  15645  gausslemma2dlem4  15937  egrsubgr  16258  bj-findis  16749