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  2905  reupick  3539  ltfinasym  4460  sfinltfin  4535  vfinspsslem1  4550  isotr  5495  qsdisj  5995  nntccl  6170  sbthlem3  6205  ltlenlec  6207  letc  6231  ncslemuc  6255  fnfrec  6320