Theorem adantrd 454

Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)

Hypothesis

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

Assertion

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

Proof of Theorem adantrd

Step	Hyp	Ref	Expression
1		simpl 443	. 2 |- ((ps /\ th) -> ps)
2		adantrd.1	. 2 |- (ph -> (ps -> ch))
3	1, 2	syl5 28	1 |- (ph -> ((ps /\ th) -> 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:  syldan  456  jaoa  496  prlem1  928  cad0  1400  equveli  1988  2eu3  2286  unineq  3506  tfinltfinlem1  4501  sfintfin  4533  vfinncvntnn  4549  fvun1  5380  fnasrn  5418  fconst5  5456  fconstfv  5457  enadjlem1  6060  leltctr  6213  addcdi  6251  nmembers1lem3  6271  nchoicelem12  6301