Theorem adantrd 273

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 107	. 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 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem is referenced by:  syldan  276  jaoa  672  prlem1  914  equveli  1682  elssabg  3923  suctr  4176  fvun1  5260  opabbrex  5569  poxp  5873  tposfo2  5905  1idprl  6780  1idpru  6781  uzind  8458  xrlttr  8870  fzen  9062  fz0fzelfz0  9138  zeqzmulgcd  10362  lcmgcdlem  10459  lcmdvds  10461  cncongr2  10486  exprmfct  10519  bj-om  10732