Theorem 3ad2antl1 1162

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

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

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 983

This theorem is referenced by:  acexmid  5945  f1oen4g  6845  f1dom4g  6846  ordiso2  7139  addlocpr  7651  distrlem1prl  7697  distrlem1pru  7698  ltsopr  7711  addcanprlemu  7730  fzo1fzo0n0  10309  pfxsuffeqwrdeq  11152  prodfap0  11889  prodfrecap  11890  muldvds2  12161  dvds2add  12169  dvds2sub  12170  dvdstr  12172  qusaddvallemg  13198  mulgnnsubcl  13503  mulgpropdg  13533  ringidss  13824  lmodprop2d  14143  cnpnei  14724  upxp  14777  lgsval4lem  15521