Theorem 3adantl1 1167

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 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  1187  3ad2antl3  1188  funcnvqp  6580  onfununi  8310  omord2  8531  en2eqpr  9960  divmuldiv  11882  ioojoin  13444  expnlbnd  14198  swrdlend  14618  2cshw  14778  lcmledvds  16569  pospropd  18286  marrepcl  22451  gsummatr01lem3  22544  upxp  23510  rnelfmlem  23839  brbtwn2  28832  wlkonprop  29586  trlsonprop  29636  pthsonprop  29674  spthonprop  29675  spthonepeq  29682  fh2  31548  homulass  31731  hoadddi  31732  hoadddir  31733  metf1o  37749  rngohomco  37968  rngoisoco  37976  op01dm  39176  paddss12  39813  wessf1ornlem  45179  elaa2  46232  smflimlem2  46770