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  7376  addlocpr  7904  distrlem1prl  7950  distrlem1pru  7951  ltsopr  7964  addcanprlemu  7983  fzo1fzo0n0  10606  pfxsuffeqwrdeq  11486  prodfap0  12331  prodfrecap  12332  muldvds2  12603  dvds2add  12611  dvds2sub  12612  dvdstr  12614  qusaddvallemg  13707  mulgnnsubcl  13990  mulgpropdg  14020  ringidss  14418  lmodprop2d  14769  issubassa  15097  cnpnei  15411  upxp  15464  lgsval4lem  16296  clwwlkccatlem  16807  clwwlkccat  16808