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  4192  suctr  4468  fvun1  5645  opabbrex  5989  poxp  6318  tposfo2  6353  1idprl  7703  1idpru  7704  uzind  9484  xrlttr  9917  fzen  10165  fz0fzelfz0  10249  ccatsymb  11058  fisumss  11703  fprodssdc  11901  zeqzmulgcd  12291  lcmgcdlem  12399  lcmdvds  12401  cncongr2  12426  exprmfct  12460  pceu  12618  infpnlem1  12682  isghm  13579  ringadd2  13789  metrest  14978  bj-charfunbi  15747  bj-om  15873