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  725  prlem1  979  equveli  1805  elssabg  4232  suctr  4512  fvun1  5700  opabbrex  6048  poxp  6378  tposfo2  6413  1idprl  7777  1idpru  7778  uzind  9558  xrlttr  9991  fzen  10239  fz0fzelfz0  10323  ccatsymb  11137  fisumss  11903  fprodssdc  12101  zeqzmulgcd  12491  lcmgcdlem  12599  lcmdvds  12601  cncongr2  12626  exprmfct  12660  pceu  12818  infpnlem1  12882  isghm  13780  ringadd2  13990  metrest  15180  umgredg  15943  bj-charfunbi  16174  bj-om  16300