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  732  prlem1  986  equveli  1812  elssabg  4279  suctr  4561  fvun1  5763  opabbrex  6122  poxp  6458  tposfo2  6528  1idprl  7947  1idpru  7948  uzind  9736  xrlttr  10176  fzen  10426  fz0fzelfz0  10512  hashf1lem2  11264  ccatsymb  11348  fisumss  12137  fprodssdc  12335  zeqzmulgcd  12725  lcmgcdlem  12833  lcmdvds  12835  cncongr2  12860  exprmfct  12894  pceu  13052  infpnlem1  13116  isghm  14023  ringadd2  14305  metrest  15530  umgredg  16300  bj-charfunbi  16751  bj-om  16877