Theorem 3adantl1 1179

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  3ad2antl2  1199  3ad2antl3  1200  funcnvqp  6580  onfununi  8306  omord2  8530  en2eqpr  9957  divmuldiv  11885  ioojoin  13481  expnlbnd  14240  swrdlend  14661  2cshw  14820  lcmledvds  16624  pospropd  18348  marrepcl  22612  gsummatr01lem3  22705  upxp  23671  rnelfmlem  24000  brbtwn2  29063  wlkonprop  29814  trlsonprop  29863  pthsonprop  29901  spthonprop  29902  spthonepeq  29909  fh2  31779  homulass  31962  hoadddi  31963  hoadddir  31964  metf1o  38215  rngohomco  38434  rngoisoco  38442  op01dm  39768  paddss12  40404  wessf1ornlem  45724  elaa2  46769  smflimlem2  47307