Theorem 3adant1l 1318

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

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

Assertion

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

Proof of Theorem 3adant1l

Step	Hyp	Ref	Expression
1		3adant1l.1	. . . 4 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3expb 1266	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	adantll 750	. 2 |- ( ( ( ta /\ ph ) /\ ( ps /\ ch ) ) -> th )
4	3	3impb 1260	1 |- ( ( ( ta /\ ph ) /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  3adant2l  1320  3adant3l  1322  cfsmolem  9092  axdc3lem4  9275  issubmnd  17318  maducoeval2  20446  cramerlem3  20495  restnlly  21285  efgh  24287  funvtxdm2valOLD  25895  funiedgdm2valOLD  25896  hasheuni  30147  matunitlindflem1  33405  pellex  37399  mendlmod  37763  disjf1o  39378  ssfiunibd  39523  mullimc  39848  mullimcf  39855  limclner  39883  limsupresxr  39998  liminfresxr  39999  sge0lefi  40615  isomenndlem  40744  hoicvr  40762  ovncvrrp  40778