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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem is used by:  syldan  282  jaoa  732  prlem1  986  equveli  1812  elssabg  4286  suctr  4568  fvun1  5772  opabbrex  6135  poxp  6472  tposfo2  6543  1idprl  7963  1idpru  7964  uzind  9767  xrlttr  10213  fzen  10463  fz0fzelfz0  10550  hashf1lem2  11307  ccatsymb  11391  fisumss  12183  fprodssdc  12381  zeqzmulgcd  12771  lcmgcdlem  12879  lcmdvds  12881  cncongr2  12906  exprmfct  12941  pceu  13102  infpnlem1  13166  prmlem0  13248  isghm  14104  ringadd2  14438  metrest  15749  bcmono  16321  umgredg  16608  bj-charfunbi  17059  bj-om  17185