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  6540  onfununi  8256  omord2  8477  en2eqpr  9893  divmuldiv  11816  ioojoin  13378  expnlbnd  14135  swrdlend  14556  2cshw  14715  lcmledvds  16505  pospropd  18226  marrepcl  22474  gsummatr01lem3  22567  upxp  23533  rnelfmlem  23862  brbtwn2  28878  wlkonprop  29630  trlsonprop  29679  pthsonprop  29717  spthonprop  29718  spthonepeq  29725  fh2  31591  homulass  31774  hoadddi  31775  hoadddir  31776  metf1o  37795  rngohomco  38014  rngoisoco  38022  op01dm  39222  paddss12  39858  wessf1ornlem  45222  elaa2  46272  smflimlem2  46810