Theorem 3ad2antl1 1190

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 481	. 2 |- ( ( ( ph /\ ta ) /\ ch ) -> th )
3	2	3adantl2 1185	1 |- ( ( ( ph /\ ps /\ ta ) /\ ch ) -> th )

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

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 1011

This theorem is referenced by:  acexmid  6074  f1oen4g  7028  f1dom4g  7029  ordiso2  7365  addlocpr  7893  distrlem1prl  7939  distrlem1pru  7940  ltsopr  7953  addcanprlemu  7972  fzo1fzo0n0  10573  pfxsuffeqwrdeq  11448  prodfap0  12290  prodfrecap  12291  muldvds2  12562  dvds2add  12570  dvds2sub  12571  dvdstr  12573  qusaddvallemg  13631  mulgnnsubcl  13914  mulgpropdg  13944  ringidss  14307  lmodprop2d  14657  cnpnei  15243  upxp  15296  lgsval4lem  16044  clwwlkccatlem  16555  clwwlkccat  16556