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  4286  suctr  4568  fvun1  5772  opabbrex  6135  poxp  6472  tposfo2  6542  1idprl  7963  1idpru  7964  uzind  9768  xrlttr  10214  fzen  10464  fz0fzelfz0  10551  hashf1lem2  11308  ccatsymb  11392  fisumss  12184  fprodssdc  12382  zeqzmulgcd  12772  lcmgcdlem  12880  lcmdvds  12882  cncongr2  12907  exprmfct  12942  pceu  13103  infpnlem1  13167  prmlem0  13249  isghm  14105  ringadd2  14439  metrest  15732  bcmono  16304  umgredg  16591  bj-charfunbi  17042  bj-om  17168