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  4233  suctr  4513  fvun1  5705  opabbrex  6057  poxp  6389  tposfo2  6424  1idprl  7793  1idpru  7794  uzind  9574  xrlttr  10008  fzen  10256  fz0fzelfz0  10340  ccatsymb  11155  fisumss  11924  fprodssdc  12122  zeqzmulgcd  12512  lcmgcdlem  12620  lcmdvds  12622  cncongr2  12647  exprmfct  12681  pceu  12839  infpnlem1  12903  isghm  13801  ringadd2  14011  metrest  15201  umgredg  15964  bj-charfunbi  16283  bj-om  16409