Theorem 3adant2l 1320

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
3adant2l	|- ( ( ph /\ ( ta /\ ps ) /\ ch ) -> th )

Proof of Theorem 3adant2l

Step	Hyp	Ref	Expression
1		3adant1l.1	. . . 4 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3com12 1269	. . 3 |- ( ( ps /\ ph /\ ch ) -> th )
3	2	3adant1l 1318	. 2 |- ( ( ( ta /\ ps ) /\ ph /\ ch ) -> th )
4	3	3com12 1269	1 |- ( ( ph /\ ( ta /\ 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:  axdc3lem4  9275  modexp  12999  lmmbr2  23057  ax5seglem1  25808  ax5seglem2  25809  nvaddsub4  27512  pl1cn  30001  athgt  34742  ltrncoelN  35429  ltrncoat  35430  trlcoabs  36009  tendoplcl2  36066  tendopltp  36068  dih1dimatlem0  36617  pellex  37399  fourierdlem42  40366