Theorem 3adantl1 1152

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

Hypothesis

Ref	Expression
3adantl.1

Assertion

Ref	Expression
3adantl1

Proof of Theorem 3adantl1

Step	Hyp	Ref	Expression
1		3simpc 995	. 2
2		3adantl.1	. 2
3	1, 2	sylan 471	1

Syntax hints:  ->wi 4  /\wa 369  /\w3a 973

This theorem is referenced by:  3ad2antl2  1159  3ad2antl3  1160  onfununi  7031  omord2  7235  en2eqpr  8406  divmuldiv  10269  ioojoin  11680  expnlbnd  12296  swrdlend  12656  pospropd  15764  marrepcl  19066  gsummatr01lem3  19159  upxp  20124  rnelfmlem  20453  brbtwn2  24208  fh2  26537  homulass  26721  hoadddi  26722  hoadddir  26723  metf1o  30248  rngohomco  30377  rngoisoco  30385  lcmledvds  31205  elaa2  32017  op01dm  34908  paddss12  35543

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 185  df-an 371  df-3an 975