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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  acexmid  6084  f1oen4g  7038  f1dom4g  7039  ordiso2  7375  addlocpr  7903  distrlem1prl  7949  distrlem1pru  7950  ltsopr  7963  addcanprlemu  7982  fzo1fzo0n0  10605  pfxsuffeqwrdeq  11484  prodfap0  12328  prodfrecap  12329  muldvds2  12600  dvds2add  12608  dvds2sub  12609  dvdstr  12611  qusaddvallemg  13703  mulgnnsubcl  13986  mulgpropdg  14016  ringidss  14383  lmodprop2d  14734  issubassa  15062  cnpnei  15369  upxp  15422  lgsval4lem  16228  clwwlkccatlem  16739  clwwlkccat  16740