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

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

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 1088

This theorem is referenced by:  3ad2antl2  1187  3ad2antl3  1188  funcnvqp  6553  onfununi  8270  omord2  8491  en2eqpr  9909  divmuldiv  11832  ioojoin  13390  expnlbnd  14147  swrdlend  14568  2cshw  14727  lcmledvds  16517  pospropd  18239  marrepcl  22499  gsummatr01lem3  22592  upxp  23558  rnelfmlem  23887  brbtwn2  28904  wlkonprop  29656  trlsonprop  29705  pthsonprop  29743  spthonprop  29744  spthonepeq  29751  fh2  31620  homulass  31803  hoadddi  31804  hoadddir  31805  metf1o  37868  rngohomco  38087  rngoisoco  38095  op01dm  39355  paddss12  39991  wessf1ornlem  45345  elaa2  46394  smflimlem2  46932