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  732  dedlema  982  dedlemb  983  prlem1  986  equveli  1812  ifnebibdc  3683  poxp  6458  ressuppss  6484  nnmordi  6779  eroprf  6892  xpdom2  7119  elni2  7671  prarloclemlo  7851  xrlttr  10176  fzen  10426  eluzgtdifelfzo  10593  ssfzo12bi  10621  climuni  12037  mulcn2  12056  serf0  12096  ntrivcvgap  12293  dfgcd2  12769  lcmgcdlem  12833  lcmdvds  12835  qnumdencl  12943  infpnlem1  13116  rng1zrlem  14233  cnplimcim  15691  dveflem  15750  gausslemma2dlem3  16096  uhgr2edg  16361  ushgredgedg  16381  ushgredgedgloop  16383  wlk1walkdom  16514  clwwlknun  16596  bj-charfundcALT  16749