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  6583  onfununi  8313  omord2  8534  en2eqpr  9967  divmuldiv  11889  ioojoin  13451  expnlbnd  14205  swrdlend  14625  2cshw  14785  lcmledvds  16576  pospropd  18293  marrepcl  22458  gsummatr01lem3  22551  upxp  23517  rnelfmlem  23846  brbtwn2  28839  wlkonprop  29593  trlsonprop  29643  pthsonprop  29681  spthonprop  29682  spthonepeq  29689  fh2  31555  homulass  31738  hoadddi  31739  hoadddir  31740  metf1o  37756  rngohomco  37975  rngoisoco  37983  op01dm  39183  paddss12  39820  wessf1ornlem  45186  elaa2  46239  smflimlem2  46777