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  5924  ordiso2  7110  addlocpr  7620  distrlem1prl  7666  distrlem1pru  7667  ltsopr  7680  addcanprlemu  7699  fzo1fzo0n0  10276  prodfap0  11727  prodfrecap  11728  muldvds2  11999  dvds2add  12007  dvds2sub  12008  dvdstr  12010  qusaddvallemg  13035  mulgnnsubcl  13340  mulgpropdg  13370  ringidss  13661  lmodprop2d  13980  cnpnei  14539  upxp  14592  lgsval4lem  15336