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  5990  cocan1  5993  acexmid  6084  caovimo  6283  ordiso2  7375  mkvprop  7498  ltpopr  7962  ltsopr  7963  addcanprleml  7981  addcanprlemu  7982  aptiprlemu  8007  seq1g  10900  dvdsmodexp  12562  muldvds1  12583  lcmdvds  12857  cnpnei  15320  upgrpredgv  16387