Theorem 3ad2antl1 1186

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 1181	1 |- ( ( ( ph /\ ps /\ ta ) /\ ch ) -> th )

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

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 1007

This theorem is referenced by:  acexmid  6057  f1oen4g  7004  f1dom4g  7005  ordiso2  7339  addlocpr  7867  distrlem1prl  7913  distrlem1pru  7914  ltsopr  7927  addcanprlemu  7946  fzo1fzo0n0  10544  pfxsuffeqwrdeq  11415  prodfap0  12256  prodfrecap  12257  muldvds2  12528  dvds2add  12536  dvds2sub  12537  dvdstr  12539  qusaddvallemg  13597  mulgnnsubcl  13887  mulgpropdg  13917  ringidss  14272  lmodprop2d  14622  cnpnei  15210  upxp  15263  lgsval4lem  16010  clwwlkccatlem  16521  clwwlkccat  16522