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  1770  elssabg  4178  suctr  4453  fvun1  5624  opabbrex  5963  poxp  6287  tposfo2  6322  1idprl  7652  1idpru  7653  uzind  9431  xrlttr  9864  fzen  10112  fz0fzelfz0  10196  fisumss  11538  fprodssdc  11736  zeqzmulgcd  12110  lcmgcdlem  12218  lcmdvds  12220  cncongr2  12245  exprmfct  12279  pceu  12436  infpnlem1  12500  isghm  13316  ringadd2  13526  metrest  14685  bj-charfunbi  15373  bj-om  15499