Theorem adantrd 277

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 108	. 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 103

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

This theorem is referenced by:  syldan  280  jaoa  715  prlem1  968  equveli  1752  elssabg  4134  suctr  4406  fvun1  5562  opabbrex  5897  poxp  6211  tposfo2  6246  1idprl  7552  1idpru  7553  uzind  9323  xrlttr  9752  fzen  9999  fz0fzelfz0  10083  fisumss  11355  fprodssdc  11553  zeqzmulgcd  11925  lcmgcdlem  12031  lcmdvds  12033  cncongr2  12058  exprmfct  12092  pceu  12249  infpnlem1  12311  metrest  13300  bj-charfunbi  13846  bj-om  13972