Theorem 3adantl1 1167

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 1151	. 2 ⊢ ((𝜏 ∧ 𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2		3adantl.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 580	1 ⊢ (((𝜏 ∧ 𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3ad2antl2  1187  3ad2antl3  1188  funcnvqp  6630  onfununi  8381  omord2  8605  en2eqpr  10047  divmuldiv  11967  ioojoin  13523  expnlbnd  14272  swrdlend  14691  2cshw  14851  lcmledvds  16636  pospropd  18372  marrepcl  22570  gsummatr01lem3  22663  upxp  23631  rnelfmlem  23960  brbtwn2  28920  wlkonprop  29676  trlsonprop  29726  pthsonprop  29764  spthonprop  29765  spthonepeq  29772  fh2  31638  homulass  31821  hoadddi  31822  hoadddir  31823  metf1o  37762  rngohomco  37981  rngoisoco  37989  op01dm  39184  paddss12  39821  wessf1ornlem  45190  elaa2  46249  smflimlem2  46787