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  1163  3adant1l  1232  reu6  2953  sbc2iegf  3060  sbcralt  3066  sbcrext  3067  indifdir  3419  pofun  4347  poinxp  4732  ssimaex  5622  fndmdif  5667  dffo4  5710  fcompt  5732  fconst2g  5777  foco2  5800  foeqcnvco  5837  f1eqcocnv  5838  fliftel1  5841  isores3  5862  acexmid  5921  tfrlemi14d  6391  tfrcl  6422  dom2lem  6831  fiintim  6992  ordiso2  7101  mkvprop  7224  lt2addnq  7471  lt2mulnq  7472  ltexnqq  7475  genpdf  7575  addnqprl  7596  addnqpru  7597  addlocpr  7603  recexprlemopl  7692  caucvgsrlemgt1  7862  add4  8187  cnegex  8204  ltleadd  8473  zextle  9417  peano5uzti  9434  fnn0ind  9442  xrlttr  9870  xaddass  9944  iccshftr  10069  iccshftl  10071  iccdil  10073  icccntr  10075  fzaddel  10134  fzrev  10159  exbtwnzlemshrink  10338  xqltnle  10357  seq3val  10552  iseqf1olemab  10594  seqf1og  10613  exp3vallem  10632  mulexp  10670  expadd  10673  expmul  10676  leexp1a  10686  bccl  10859  hashfacen  10928  wrdnval  10965  ovshftex  10984  2shfti  10996  caucvgre  11146  cvg1nlemcau  11149  resqrexlemcvg  11184  cau3lem  11279  rexico  11386  iooinsup  11442  climmpt  11465  subcn2  11476  climrecvg1n  11513  climcvg1nlem  11514  climcaucn  11516  mertenslem2  11701  eftlcl  11853  reeftlcl  11854  dvdsext  12020  3dvds  12029  sqoddm1div8z  12051  bezoutlemaz  12170  bezoutr1  12200  dvdslcm  12237  lcmeq0  12239  lcmcl  12240  lcmneg  12242  lcmdvds  12247  coprmgcdb  12256  dvdsprime  12290  pc2dvds  12499  prmpwdvds  12524  infpnlem1  12528  1arith  12536  resmhm  13119  resmhm2b  13121  mhmco  13122  mhmima  13123  gsumwsubmcl  13128  dfgrp2  13159  mulgfng  13254  subgintm  13328  ghmmhmb  13384  resghm  13390  islmod  13847  islmodd  13849  cnco  14457  cnss1  14462  tx2cn  14506  upxp  14508  metss  14730  txmetcnp  14754  cncfss  14819  plyaddlem1  14983  plymullem1  14984  cosz12  15016  gausslemma2dlem4  15305  bj-findis  15625