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  6609  tfrcl  6640  mapsnd  6976  dom2lem  7064  fiintim  7244  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  9747  peano5uzti  9764  fnn0ind  9772  xrlttr  10213  xaddass  10287  iccshftr  10412  iccshftl  10414  iccdil  10416  icccntr  10418  fzaddel  10481  fzrev  10507  exbtwnzlemshrink  10699  xqltnle  10718  seq3val  10917  iseqf1olemab  10959  seqf1og  10978  exp3vallem  10997  mulexp  11035  expadd  11038  expmul  11041  leexp1a  11051  bccl  11226  hashfacen  11305  wrdnval  11356  swrdccat3blem  11532  ovshftex  11605  2shfti  11617  caucvgre  11768  cvg1nlemcau  11771  resqrexlemcvg  11806  cau3lem  11902  rexico  12009  iooinsup  12067  climmpt  12090  subcn2  12101  climrecvg1n  12138  climcvg1nlem  12139  climcaucn  12141  mertenslem2  12327  eftlcl  12479  reeftlcl  12480  dvdsext  12646  3dvds  12655  sqoddm1div8z  12677  bezoutlemaz  12804  bezoutr1  12834  dvdslcm  12871  lcmeq0  12873  lcmcl  12874  lcmneg  12876  lcmdvds  12881  coprmgcdb  12890  dvdsprime  12924  pc2dvds  13137  prmpwdvds  13162  infpnlem1  13166  1arith  13174  resmhm  13852  resmhm2b  13854  mhmco  13855  mhmima  13856  gzsumwsubmcl  13859  dfgrp2  13890  mulgfng  13985  subgintm  14059  ghmmhmb  14115  resghm  14121  cntzmhm  14172  islmod  14735  islmodd  14737  psrdifi  15211  psrdirfi  15212  cnco  15464  cnss1  15469  tx2cn  15513  upxp  15515  metss  15737  txmetcnp  15761  cncfss  15826  plyaddlem1  15990  plymullem1  15991  cosz12  16024  bposlem3  16330  gausslemma2dlem4  16405  egrsubgr  16726  bj-findis  17227