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  3505  tfinltfinlem1  4500  sfintfin  4532  vfinncvntnn  4548  fvun1  5379  fnasrn  5417  fconst5  5455  fconstfv  5456  enadjlem1  6059  leltctr  6212  addcdi  6250  nmembers1lem3  6270  nchoicelem12  6300