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  7376  mkvprop  7499  ltpopr  7963  ltsopr  7964  addcanprleml  7982  addcanprlemu  7983  aptiprlemu  8008  seq1g  10915  dvdsmodexp  12581  muldvds1  12602  lcmdvds  12876  cnpnei  15411  upgrpredgv  16553