Theorem adantll 480

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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad2antlr  493  ad2ant2l  512  ad2ant2lr  514  ad5ant23  526  ad5ant24  527  ad5ant25  528  3ad2antl3  1192  3adant1l  1261  reu6  3015  sbc2iegf  3122  sbcralt  3128  sbcrext  3129  indifdir  3487  sn0disj  4127  pofun  4459  poinxp  4846  ssimaex  5767  fndmdif  5817  dffo4  5859  fcompt  5881  fconst2g  5933  foco2  5962  foeqcnvco  5999  f1eqcocnv  6000  fliftel1  6003  isores3  6024  acexmid  6087  suppssdc  6504  tfrlemi14d  6608  tfrcl  6639  mapsnd  6974  dom2lem  7062  fiintim  7242  ordiso2  7381  mkvprop  7504  lt2addnq  7777  lt2mulnq  7778  ltexnqq  7781  genpdf  7881  addnqprl  7902  addnqpru  7903  addlocpr  7909  recexprlemopl  7998  caucvgsrlemgt1  8168  add4  8494  cnegex  8511  ltleadd  8781  zextle  9748  peano5uzti  9765  fnn0ind  9773  xrlttr  10214  xaddass  10288  iccshftr  10413  iccshftl  10415  iccdil  10417  icccntr  10419  fzaddel  10482  fzrev  10508  exbtwnzlemshrink  10700  xqltnle  10719  seq3val  10918  iseqf1olemab  10960  seqf1og  10979  exp3vallem  10998  mulexp  11036  expadd  11039  expmul  11042  leexp1a  11052  bccl  11227  hashfacen  11306  wrdnval  11357  swrdccat3blem  11533  ovshftex  11606  2shfti  11618  caucvgre  11769  cvg1nlemcau  11772  resqrexlemcvg  11807  cau3lem  11903  rexico  12010  iooinsup  12068  climmpt  12091  subcn2  12102  climrecvg1n  12139  climcvg1nlem  12140  climcaucn  12142  mertenslem2  12328  eftlcl  12480  reeftlcl  12481  dvdsext  12647  3dvds  12656  sqoddm1div8z  12678  bezoutlemaz  12805  bezoutr1  12835  dvdslcm  12872  lcmeq0  12874  lcmcl  12875  lcmneg  12877  lcmdvds  12882  coprmgcdb  12891  dvdsprime  12925  pc2dvds  13138  prmpwdvds  13163  infpnlem1  13167  1arith  13175  resmhm  13853  resmhm2b  13855  mhmco  13856  mhmima  13857  gzsumwsubmcl  13860  dfgrp2  13891  mulgfng  13986  subgintm  14060  ghmmhmb  14116  resghm  14122  cntzmhm  14173  islmod  14736  islmodd  14738  psrdifi  15202  psrdirfi  15203  cnco  15447  cnss1  15452  tx2cn  15496  upxp  15498  metss  15720  txmetcnp  15744  cncfss  15809  plyaddlem1  15973  plymullem1  15974  cosz12  16007  bposlem3  16313  gausslemma2dlem4  16388  egrsubgr  16709  bj-findis  17210