Theorem ad2antrr 706

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)

Hypothesis

Ref	Expression
ad2ant.1	|- (ph -> ps)

Assertion

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

Proof of Theorem ad2antrr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- (ph -> ps)
2	1	adantr 451	. 2 |- ((ph /\ th) -> ps)
3	2	adantlr 695	1 |- (((ph /\ ch) /\ th) -> ps)

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:  ad3antrrr  710  simpll  730  simplll  734  simpllr  735  ax11eq  2193  ax11el  2194  ax11indalem  2197  ax11inda2ALT  2198  vtoclgft  2906  reupick  3540  ltfinasym  4461  sfinltfin  4536  vfinspsslem1  4551  isotr  5496  qsdisj  5996  nntccl  6171  sbthlem3  6206  ltlenlec  6208  letc  6232  ncslemuc  6256  fnfrec  6321