Theorem adantll 468

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 109	. 2 |- ( ( th /\ ph ) -> ph )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan 281	1 |- ( ( ( th /\ ph ) /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad2antlr  481  ad2ant2l  500  ad2ant2lr  502  ad5ant23  514  ad5ant24  515  ad5ant25  516  3ad2antl3  1151  3adant1l  1220  reu6  2915  sbc2iegf  3021  sbcralt  3027  sbcrext  3028  indifdir  3378  pofun  4290  poinxp  4673  ssimaex  5547  fndmdif  5590  dffo4  5633  fcompt  5655  fconst2g  5700  foco2  5722  foeqcnvco  5758  f1eqcocnv  5759  fliftel1  5762  isores3  5783  acexmid  5841  tfrlemi14d  6301  tfrcl  6332  dom2lem  6738  fiintim  6894  ordiso2  7000  mkvprop  7122  lt2addnq  7345  lt2mulnq  7346  ltexnqq  7349  genpdf  7449  addnqprl  7470  addnqpru  7471  addlocpr  7477  recexprlemopl  7566  caucvgsrlemgt1  7736  add4  8059  cnegex  8076  ltleadd  8344  zextle  9282  peano5uzti  9299  fnn0ind  9307  xrlttr  9731  xaddass  9805  iccshftr  9930  iccshftl  9932  iccdil  9934  icccntr  9936  fzaddel  9994  fzrev  10019  exbtwnzlemshrink  10184  seq3val  10393  iseqf1olemab  10424  exp3vallem  10456  mulexp  10494  expadd  10497  expmul  10500  leexp1a  10510  bccl  10680  hashfacen  10749  ovshftex  10761  2shfti  10773  caucvgre  10923  cvg1nlemcau  10926  resqrexlemcvg  10961  cau3lem  11056  rexico  11163  iooinsup  11218  climmpt  11241  subcn2  11252  climrecvg1n  11289  climcvg1nlem  11290  climcaucn  11292  mertenslem2  11477  eftlcl  11629  reeftlcl  11630  dvdsext  11793  sqoddm1div8z  11823  bezoutlemaz  11936  bezoutr1  11966  dvdslcm  12001  lcmeq0  12003  lcmcl  12004  lcmneg  12006  lcmdvds  12011  coprmgcdb  12020  dvdsprime  12054  pc2dvds  12261  prmpwdvds  12285  infpnlem1  12289  1arith  12297  cnco  12861  cnss1  12866  tx2cn  12910  upxp  12912  metss  13134  txmetcnp  13158  cncfss  13210  cosz12  13341  bj-findis  13861