Theorem 3adantl1 1237

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

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

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  3ad2antl2  1244  3ad2antl3  1245  funcnvqp  5990  onfununi  7483  omord2  7692  en2eqpr  8868  divmuldiv  10763  ioojoin  12341  expnlbnd  13034  swrdlend  13477  lcmledvds  15359  pospropd  17181  marrepcl  20418  gsummatr01lem3  20511  upxp  21474  rnelfmlem  21803  brbtwn2  25830  spthonepeq  26704  fh2  28606  homulass  28789  hoadddi  28790  hoadddir  28791  metf1o  33681  rngohomco  33903  rngoisoco  33911  op01dm  34788  paddss12  35423  wessf1ornlem  39685  elaa2  40769  smflimlem2  41301