Theorem 3adantl1 1217

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)

Hypothesis

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

Assertion

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

Proof of Theorem 3adantl1

Step	Hyp	Ref	Expression
1		3simpc 1060	. 2 |- ( ( ta /\ ph /\ ps ) -> ( ph /\ ps ) )
2		3adantl.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylan 488	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:  3ad2antl2  1224  3ad2antl3  1225  funcnvqp  5952  onfununi  7438  omord2  7647  en2eqpr  8830  divmuldiv  10725  ioojoin  12303  expnlbnd  12994  swrdlend  13431  lcmledvds  15312  pospropd  17134  marrepcl  20370  gsummatr01lem3  20463  upxp  21426  rnelfmlem  21756  brbtwn2  25785  spthonepeq  26648  fh2  28478  homulass  28661  hoadddi  28662  hoadddir  28663  metf1o  33551  rngohomco  33773  rngoisoco  33781  op01dm  34470  paddss12  35105  wessf1ornlem  39371  elaa2  40451  smflimlem2  40980