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 )

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:  fcofo  5993  cocan1  5996  acexmid  6087  caovimo  6286  ordiso2  7381  mkvprop  7504  ltpopr  7968  ltsopr  7969  addcanprleml  7987  addcanprlemu  7988  aptiprlemu  8013  seq1g  10920  dvdsmodexp  12586  muldvds1  12607  lcmdvds  12881  cnpnei  15462  upgrpredgv  16609