Theorem 3ad2antl1 1159

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

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

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 980

This theorem is referenced by:  acexmid  5876  ordiso2  7036  addlocpr  7537  distrlem1prl  7583  distrlem1pru  7584  ltsopr  7597  addcanprlemu  7616  fzo1fzo0n0  10185  prodfap0  11555  prodfrecap  11556  muldvds2  11826  dvds2add  11834  dvds2sub  11835  dvdstr  11837  qusaddvallemg  12757  mulgnnsubcl  13000  mulgpropdg  13030  ringidss  13217  lmodprop2d  13443  cnpnei  13804  upxp  13857  lgsval4lem  14497