Theorem 3ad2antl1 1190

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 481	. 2 |- ( ( ( ph /\ ta ) /\ ch ) -> th )
3	2	3adantl2 1185	1 |- ( ( ( ph /\ ps /\ ta ) /\ ch ) -> th )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  acexmid  6084  f1oen4g  7038  f1dom4g  7039  ordiso2  7375  addlocpr  7903  distrlem1prl  7949  distrlem1pru  7950  ltsopr  7963  addcanprlemu  7982  fzo1fzo0n0  10595  pfxsuffeqwrdeq  11470  prodfap0  12312  prodfrecap  12313  muldvds2  12584  dvds2add  12592  dvds2sub  12593  dvdstr  12595  qusaddvallemg  13654  mulgnnsubcl  13937  mulgpropdg  13967  ringidss  14334  lmodprop2d  14685  issubassa  15013  cnpnei  15320  upxp  15373  lgsval4lem  16130  clwwlkccatlem  16641  clwwlkccat  16642