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  1783  elssabg  4208  suctr  4486  fvun1  5668  opabbrex  6012  poxp  6341  tposfo2  6376  1idprl  7738  1idpru  7739  uzind  9519  xrlttr  9952  fzen  10200  fz0fzelfz0  10284  ccatsymb  11096  fisumss  11818  fprodssdc  12016  zeqzmulgcd  12406  lcmgcdlem  12514  lcmdvds  12516  cncongr2  12541  exprmfct  12575  pceu  12733  infpnlem1  12797  isghm  13694  ringadd2  13904  metrest  15093  umgredg  15849  bj-charfunbi  15946  bj-om  16072