Theorem 3adantl1 1168

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 581	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  1188  3ad2antl3  1189  funcnvqp  6564  onfununi  8283  omord2  8504  en2eqpr  9929  divmuldiv  11853  ioojoin  13411  expnlbnd  14168  swrdlend  14589  2cshw  14748  lcmledvds  16538  pospropd  18260  marrepcl  22520  gsummatr01lem3  22613  upxp  23579  rnelfmlem  23908  brbtwn2  28990  wlkonprop  29742  trlsonprop  29791  pthsonprop  29829  spthonprop  29830  spthonepeq  29837  fh2  31707  homulass  31890  hoadddi  31891  hoadddir  31892  metf1o  38006  rngohomco  38225  rngoisoco  38233  op01dm  39559  paddss12  40195  wessf1ornlem  45544  elaa2  46592  smflimlem2  47130