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  722  prlem1  976  equveli  1782  elssabg  4193  suctr  4469  fvun1  5647  opabbrex  5991  poxp  6320  tposfo2  6355  1idprl  7705  1idpru  7706  uzind  9486  xrlttr  9919  fzen  10167  fz0fzelfz0  10251  ccatsymb  11061  fisumss  11736  fprodssdc  11934  zeqzmulgcd  12324  lcmgcdlem  12432  lcmdvds  12434  cncongr2  12459  exprmfct  12493  pceu  12651  infpnlem1  12715  isghm  13612  ringadd2  13822  metrest  15011  bj-charfunbi  15784  bj-om  15910