Theorem adantrd 277

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 108	. 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 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem is referenced by:  syldan  280  jaoa  710  prlem1  963  equveli  1747  elssabg  4126  suctr  4398  fvun1  5551  opabbrex  5882  poxp  6196  tposfo2  6231  1idprl  7527  1idpru  7528  uzind  9298  xrlttr  9727  fzen  9974  fz0fzelfz0  10058  fisumss  11329  fprodssdc  11527  zeqzmulgcd  11899  lcmgcdlem  12005  lcmdvds  12007  cncongr2  12032  exprmfct  12066  pceu  12223  infpnlem1  12285  metrest  13106  bj-charfunbi  13653  bj-om  13779