Theorem adantll 465

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 279	1 |- ( ( ( th /\ ph ) /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  ad2antlr  478  ad2ant2l  497  ad2ant2lr  499  3ad2antl3  1128  3adant1l  1191  reu6  2842  sbc2iegf  2947  sbcralt  2953  sbcrext  2954  indifdir  3298  pofun  4194  poinxp  4568  ssimaex  5436  fndmdif  5479  dffo4  5522  fcompt  5544  fconst2g  5589  foco2  5609  foeqcnvco  5645  f1eqcocnv  5646  fliftel1  5649  isores3  5670  acexmid  5727  tfrlemi14d  6184  tfrcl  6215  dom2lem  6620  fiintim  6770  ordiso2  6872  mkvprop  6982  lt2addnq  7160  lt2mulnq  7161  ltexnqq  7164  genpdf  7264  addnqprl  7285  addnqpru  7286  addlocpr  7292  recexprlemopl  7381  caucvgsrlemgt1  7537  add4  7846  cnegex  7863  ltleadd  8127  zextle  9046  peano5uzti  9063  fnn0ind  9071  xrlttr  9474  xaddass  9545  iccshftr  9670  iccshftl  9672  iccdil  9674  icccntr  9676  fzaddel  9732  fzrev  9757  exbtwnzlemshrink  9919  seq3val  10124  iseqf1olemab  10155  exp3vallem  10187  mulexp  10225  expadd  10228  expmul  10231  leexp1a  10241  bccl  10406  hashfacen  10472  ovshftex  10484  2shfti  10496  caucvgre  10645  cvg1nlemcau  10648  resqrexlemcvg  10683  cau3lem  10778  rexico  10885  iooinsup  10938  climmpt  10961  subcn2  10972  climrecvg1n  11009  climcvg1nlem  11010  climcaucn  11012  mertenslem2  11197  eftlcl  11245  reeftlcl  11246  dvdsext  11401  sqoddm1div8z  11431  bezoutlemaz  11537  bezoutr1  11567  dvdslcm  11596  lcmeq0  11598  lcmcl  11599  lcmneg  11601  lcmdvds  11606  coprmgcdb  11615  dvdsprime  11649  cnco  12232  cnss1  12237  tx2cn  12281  upxp  12283  metss  12483  txmetcnp  12507  cncfss  12556  bj-findis  12869