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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem is used by:  syldan  282  jaoa  732  prlem1  986  equveli  1812  elssabg  4284  suctr  4566  fvun1  5769  opabbrex  6132  poxp  6468  tposfo2  6538  1idprl  7957  1idpru  7958  uzind  9761  xrlttr  10207  fzen  10457  fz0fzelfz0  10544  hashf1lem2  11300  ccatsymb  11384  fisumss  12175  fprodssdc  12373  zeqzmulgcd  12763  lcmgcdlem  12871  lcmdvds  12873  cncongr2  12898  exprmfct  12933  pceu  13094  infpnlem1  13158  prmlem0  13240  isghm  14095  ringadd2  14381  metrest  15656  bcmono  16202  umgredg  16484  bj-charfunbi  16935  bj-om  17061