Theorem adantrd 275

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 108	. 2 |- ( ( ps /\ th ) -> ps )
2		adantrd.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5 32	1 |- ( ph -> ( ( ps /\ th ) -> ch ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem is referenced by:  syldan  278  jaoa  692  prlem1  940  equveli  1715  elssabg  4033  suctr  4303  fvun1  5441  opabbrex  5769  poxp  6083  tposfo2  6118  1idprl  7346  1idpru  7347  uzind  9066  xrlttr  9474  fzen  9716  fz0fzelfz0  9797  fisumss  11053  zeqzmulgcd  11507  lcmgcdlem  11604  lcmdvds  11606  cncongr2  11631  exprmfct  11664  metrest  12495  bj-om  12827