Theorem adantrr 697

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
adantrr	|- ((ph /\ (ps /\ th)) -> ch)

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		simpl 443	. 2 |- ((ps /\ th) -> ps)
2		adant2.1	. 2 |- ((ph /\ ps) -> ch)
3	1, 2	sylan2 460	1 |- ((ph /\ (ps /\ th)) -> ch)

Syntax hints:   -> wi 4   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  ad2ant2r  727  ad2ant2lr  728  consensus  925  3ad2antr1  1120  sbcom  2089  ax11eq  2193  ax11el  2194  nndisjeq  4430  tfinpw1  4495  tfinsuc  4499  sfindbl  4531  vfinspsslem1  4551  isocnv  5492  isores2  5494  isoini  5498  f1oiso2  5501  ncspw1eu  6160  addccan2nc  6266  frecxp  6315  fnfrec  6321