Theorem adantrd 279

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 109	. 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 104

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

This theorem is referenced by:  syldan  282  jaoa  721  prlem1  975  equveli  1773  elssabg  4182  suctr  4457  fvun1  5630  opabbrex  5970  poxp  6299  tposfo2  6334  1idprl  7674  1idpru  7675  uzind  9454  xrlttr  9887  fzen  10135  fz0fzelfz0  10219  fisumss  11574  fprodssdc  11772  zeqzmulgcd  12162  lcmgcdlem  12270  lcmdvds  12272  cncongr2  12297  exprmfct  12331  pceu  12489  infpnlem1  12553  isghm  13449  ringadd2  13659  metrest  14826  bj-charfunbi  15541  bj-om  15667