Theorem adantld 278

Description: Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.)

Hypothesis

Ref	Expression
adantld.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
adantld	|- ( ph -> ( ( th /\ ps ) -> ch ) )

Proof of Theorem adantld

Step	Hyp	Ref	Expression
1		simpr 110	. 2 |- ( ( th /\ ps ) -> ps )
2		adantld.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5 32	1 |- ( ph -> ( ( th /\ ps ) -> ch ) )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  jaoa  722  dedlema  972  dedlemb  973  prlem1  976  equveli  1783  ifnebibdc  3625  poxp  6341  nnmordi  6625  eroprf  6738  xpdom2  6951  elni2  7462  prarloclemlo  7642  xrlttr  9952  fzen  10200  eluzgtdifelfzo  10363  ssfzo12bi  10391  climuni  11719  mulcn2  11738  serf0  11778  ntrivcvgap  11974  dfgcd2  12450  lcmgcdlem  12514  lcmdvds  12516  qnumdencl  12624  infpnlem1  12797  cnplimcim  15254  dveflem  15313  gausslemma2dlem3  15655  bj-charfundcALT  15944