Theorem 3ad2antl1 1161

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

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

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 982

This theorem is referenced by:  acexmid  5922  ordiso2  7102  addlocpr  7605  distrlem1prl  7651  distrlem1pru  7652  ltsopr  7665  addcanprlemu  7684  fzo1fzo0n0  10261  prodfap0  11712  prodfrecap  11713  muldvds2  11984  dvds2add  11992  dvds2sub  11993  dvdstr  11995  qusaddvallemg  12986  mulgnnsubcl  13274  mulgpropdg  13304  ringidss  13595  lmodprop2d  13914  cnpnei  14465  upxp  14518  lgsval4lem  15262