Theorem 3adantl1 1165

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 1149	. 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  1185  3ad2antl3  1186  funcnvqp  6632  onfununi  8380  omord2  8604  en2eqpr  10045  divmuldiv  11965  ioojoin  13520  expnlbnd  14269  swrdlend  14688  2cshw  14848  lcmledvds  16633  pospropd  18385  marrepcl  22586  gsummatr01lem3  22679  upxp  23647  rnelfmlem  23976  brbtwn2  28935  wlkonprop  29691  trlsonprop  29741  pthsonprop  29777  spthonprop  29778  spthonepeq  29785  fh2  31648  homulass  31831  hoadddi  31832  hoadddir  31833  metf1o  37742  rngohomco  37961  rngoisoco  37969  op01dm  39165  paddss12  39802  wessf1ornlem  45128  elaa2  46190  smflimlem2  46728