Theorem 3ad2antl1 1161

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	|- ( ( ph /\ ch ) -> th )

Assertion

Ref	Expression
3ad2antl1	|- ( ( ( ph /\ ps /\ ta ) /\ ch ) -> th )

Proof of Theorem 3ad2antl1

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 |- ( ( ph /\ ch ) -> th )
2	1	adantlr 477	. 2 |- ( ( ( ph /\ ta ) /\ ch ) -> th )
3	2	3adantl2 1156	1 |- ( ( ( ph /\ ps /\ ta ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  acexmid  5921  ordiso2  7101  addlocpr  7603  distrlem1prl  7649  distrlem1pru  7650  ltsopr  7663  addcanprlemu  7682  fzo1fzo0n0  10259  prodfap0  11710  prodfrecap  11711  muldvds2  11982  dvds2add  11990  dvds2sub  11991  dvdstr  11993  qusaddvallemg  12976  mulgnnsubcl  13264  mulgpropdg  13294  ringidss  13585  lmodprop2d  13904  cnpnei  14455  upxp  14508  lgsval4lem  15252