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  4177  suctr  4452  fvun1  5623  opabbrex  5962  poxp  6285  tposfo2  6320  1idprl  7650  1idpru  7651  uzind  9428  xrlttr  9861  fzen  10109  fz0fzelfz0  10193  fisumss  11535  fprodssdc  11733  zeqzmulgcd  12107  lcmgcdlem  12215  lcmdvds  12217  cncongr2  12242  exprmfct  12276  pceu  12433  infpnlem1  12497  isghm  13313  ringadd2  13523  metrest  14674  bj-charfunbi  15303  bj-om  15429