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  721  prlem1  975  equveli  1773  elssabg  4181  suctr  4456  fvun1  5627  opabbrex  5966  poxp  6290  tposfo2  6325  1idprl  7657  1idpru  7658  uzind  9437  xrlttr  9870  fzen  10118  fz0fzelfz0  10202  fisumss  11557  fprodssdc  11755  zeqzmulgcd  12137  lcmgcdlem  12245  lcmdvds  12247  cncongr2  12272  exprmfct  12306  pceu  12464  infpnlem1  12528  isghm  13373  ringadd2  13583  metrest  14742  bj-charfunbi  15457  bj-om  15583