Theorem 3adantl1 1210

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3ad2antl2  1217  3ad2antl3  1218  funcnvqp  5866  onfununi  7325  omord2  7534  en2eqpr  8713  divmuldiv  10604  ioojoin  12174  expnlbnd  12856  swrdlend  13283  lcmledvds  15150  pospropd  16957  marrepcl  20189  gsummatr01lem3  20282  upxp  21236  rnelfmlem  21566  brbtwn2  25585  fh2  27862  homulass  28045  hoadddi  28046  hoadddir  28047  metf1o  32721  rngohomco  32943  rngoisoco  32951  op01dm  33488  paddss12  34123  wessf1ornlem  38366  elaa2  39127  smflimlem2  39658  spthonepeq-av  40958