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  1185  3adant1l  1254  reu6  2992  sbc2iegf  3099  sbcralt  3105  sbcrext  3106  indifdir  3460  pofun  4403  poinxp  4788  ssimaex  5697  fndmdif  5742  dffo4  5785  fcompt  5807  fconst2g  5858  foco2  5883  foeqcnvco  5920  f1eqcocnv  5921  fliftel1  5924  isores3  5945  acexmid  6006  tfrlemi14d  6485  tfrcl  6516  dom2lem  6931  fiintim  7104  ordiso2  7213  mkvprop  7336  lt2addnq  7602  lt2mulnq  7603  ltexnqq  7606  genpdf  7706  addnqprl  7727  addnqpru  7728  addlocpr  7734  recexprlemopl  7823  caucvgsrlemgt1  7993  add4  8318  cnegex  8335  ltleadd  8604  zextle  9549  peano5uzti  9566  fnn0ind  9574  xrlttr  10003  xaddass  10077  iccshftr  10202  iccshftl  10204  iccdil  10206  icccntr  10208  fzaddel  10267  fzrev  10292  exbtwnzlemshrink  10480  xqltnle  10499  seq3val  10694  iseqf1olemab  10736  seqf1og  10755  exp3vallem  10774  mulexp  10812  expadd  10815  expmul  10818  leexp1a  10828  bccl  11001  hashfacen  11071  wrdnval  11115  swrdccat3blem  11287  ovshftex  11346  2shfti  11358  caucvgre  11508  cvg1nlemcau  11511  resqrexlemcvg  11546  cau3lem  11641  rexico  11748  iooinsup  11804  climmpt  11827  subcn2  11838  climrecvg1n  11875  climcvg1nlem  11876  climcaucn  11878  mertenslem2  12063  eftlcl  12215  reeftlcl  12216  dvdsext  12382  3dvds  12391  sqoddm1div8z  12413  bezoutlemaz  12540  bezoutr1  12570  dvdslcm  12607  lcmeq0  12609  lcmcl  12610  lcmneg  12612  lcmdvds  12617  coprmgcdb  12626  dvdsprime  12660  pc2dvds  12869  prmpwdvds  12894  infpnlem1  12898  1arith  12906  resmhm  13536  resmhm2b  13538  mhmco  13539  mhmima  13540  gsumwsubmcl  13545  dfgrp2  13576  mulgfng  13677  subgintm  13751  ghmmhmb  13807  resghm  13813  islmod  14271  islmodd  14273  cnco  14911  cnss1  14916  tx2cn  14960  upxp  14962  metss  15184  txmetcnp  15208  cncfss  15273  plyaddlem1  15437  plymullem1  15438  cosz12  15470  gausslemma2dlem4  15759  bj-findis  16425