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  728  prlem1  982  equveli  1807  elssabg  4243  suctr  4524  fvun1  5721  opabbrex  6075  poxp  6406  tposfo2  6476  1idprl  7870  1idpru  7871  uzind  9652  xrlttr  10091  fzen  10340  fz0fzelfz0  10424  ccatsymb  11245  fisumss  12033  fprodssdc  12231  zeqzmulgcd  12621  lcmgcdlem  12729  lcmdvds  12731  cncongr2  12756  exprmfct  12790  pceu  12948  infpnlem1  13012  isghm  13910  ringadd2  14121  metrest  15317  umgredg  16086  bj-charfunbi  16527  bj-om  16653