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  958  equveli  1736  elssabg  4105  suctr  4376  fvun1  5527  opabbrex  5855  poxp  6169  tposfo2  6204  1idprl  7489  1idpru  7490  uzind  9254  xrlttr  9680  fzen  9923  fz0fzelfz0  10004  fisumss  11266  fprodssdc  11464  zeqzmulgcd  11826  lcmgcdlem  11925  lcmdvds  11927  cncongr2  11952  exprmfct  11985  metrest  12845  bj-charfunbi  13324  bj-om  13450