Theorem 3ad2antl1 1183

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

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

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 1004

This theorem is referenced by:  acexmid  6000  f1oen4g  6903  f1dom4g  6904  ordiso2  7202  addlocpr  7723  distrlem1prl  7769  distrlem1pru  7770  ltsopr  7783  addcanprlemu  7802  fzo1fzo0n0  10383  pfxsuffeqwrdeq  11230  prodfap0  12056  prodfrecap  12057  muldvds2  12328  dvds2add  12336  dvds2sub  12337  dvdstr  12339  qusaddvallemg  13366  mulgnnsubcl  13671  mulgpropdg  13701  ringidss  13992  lmodprop2d  14312  cnpnei  14893  upxp  14946  lgsval4lem  15690