Theorem 3ad2antl2 1191

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	|- ( ( ph /\ ch ) -> th )

Assertion

Ref	Expression
3ad2antl2	|- ( ( ( ps /\ ph /\ ta ) /\ ch ) -> th )

Proof of Theorem 3ad2antl2

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 |- ( ( ph /\ ch ) -> th )
2	1	adantlr 481	. 2 |- ( ( ( ph /\ ta ) /\ ch ) -> th )
3	2	3adantl1 1184	1 |- ( ( ( ps /\ ph /\ ta ) /\ ch ) -> th )

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

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 1011

This theorem is referenced by:  fcofo  5980  cocan1  5983  acexmid  6074  caovimo  6273  ordiso2  7365  mkvprop  7488  ltpopr  7952  ltsopr  7953  addcanprleml  7971  addcanprlemu  7972  aptiprlemu  7997  seq1g  10878  dvdsmodexp  12540  muldvds1  12561  lcmdvds  12835  cnpnei  15243  upgrpredgv  16301