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  6087  f1oen4g  7042  f1dom4g  7043  ordiso2  7381  addlocpr  7909  distrlem1prl  7955  distrlem1pru  7956  ltsopr  7969  addcanprlemu  7988  fzo1fzo0n0  10612  pfxsuffeqwrdeq  11492  prodfap0  12337  prodfrecap  12338  muldvds2  12609  dvds2add  12617  dvds2sub  12618  dvdstr  12620  qusaddvallemg  13713  mulgnnsubcl  13996  mulgpropdg  14026  ringidss  14441  lmodprop2d  14794  issubassa  15122  cnpnei  15445  upxp  15498  lgsval4lem  16335  clwwlkccatlem  16846  clwwlkccat  16847