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  5917  ordiso2  7094  addlocpr  7596  distrlem1prl  7642  distrlem1pru  7643  ltsopr  7656  addcanprlemu  7675  fzo1fzo0n0  10250  prodfap0  11688  prodfrecap  11689  muldvds2  11960  dvds2add  11968  dvds2sub  11969  dvdstr  11971  qusaddvallemg  12916  mulgnnsubcl  13204  mulgpropdg  13234  ringidss  13525  lmodprop2d  13844  cnpnei  14387  upxp  14440  lgsval4lem  15127