Theorem adantld 453

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 447	. 2 |- ((th /\ ps) -> ps)
2		adantld.1	. 2 |- (ph -> (ps -> ch))
3	1, 2	syl5 28	1 |- (ph -> ((th /\ ps) -> ch))

Syntax hints:   -> wi 4   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  jaoa  496  dedlema  920  dedlemb  921  prlem1  928  spimed  1977  equveli  1988  2eu3  2286  unineq  3506  tfinpw1  4495  tfinltfinlem1  4501  sfinltfin  4536  spfinsfincl  4540  vfinspsslem1  4551  clos1conn  5880  taddc  6230  nchoicelem12  6301