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  728  prlem1  982  equveli  1808  elssabg  4260  suctr  4542  fvun1  5743  opabbrex  6097  poxp  6428  tposfo2  6498  1idprl  7905  1idpru  7906  uzind  9689  xrlttr  10128  fzen  10377  fz0fzelfz0  10461  ccatsymb  11290  fisumss  12078  fprodssdc  12276  zeqzmulgcd  12666  lcmgcdlem  12774  lcmdvds  12776  cncongr2  12801  exprmfct  12835  pceu  12993  infpnlem1  13057  isghm  13960  ringadd2  14171  metrest  15371  umgredg  16140  bj-charfunbi  16581  bj-om  16707