Theorem 3adantl1 1166

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 579	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  1186  3ad2antl3  1187  funcnvqp  6642  onfununi  8397  omord2  8623  en2eqpr  10076  divmuldiv  11994  ioojoin  13543  expnlbnd  14282  swrdlend  14701  2cshw  14861  lcmledvds  16646  pospropd  18397  marrepcl  22591  gsummatr01lem3  22684  upxp  23652  rnelfmlem  23981  brbtwn2  28938  wlkonprop  29694  trlsonprop  29744  pthsonprop  29780  spthonprop  29781  spthonepeq  29788  fh2  31651  homulass  31834  hoadddi  31835  hoadddir  31836  metf1o  37715  rngohomco  37934  rngoisoco  37942  op01dm  39139  paddss12  39776  wessf1ornlem  45092  elaa2  46155  smflimlem2  46693