Theorem 3adantl1 1168

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 1151	. 2 ⊢ ((𝜏 ∧ 𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2		3adantl.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 581	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  1188  3ad2antl3  1189  funcnvqp  6556  onfununi  8274  omord2  8495  en2eqpr  9920  divmuldiv  11846  ioojoin  13427  expnlbnd  14186  swrdlend  14607  2cshw  14766  lcmledvds  16559  pospropd  18282  marrepcl  22539  gsummatr01lem3  22632  upxp  23598  rnelfmlem  23927  brbtwn2  28988  wlkonprop  29740  trlsonprop  29789  pthsonprop  29827  spthonprop  29828  spthonepeq  29835  fh2  31705  homulass  31888  hoadddi  31889  hoadddir  31890  metf1o  38090  rngohomco  38309  rngoisoco  38317  op01dm  39643  paddss12  40279  wessf1ornlem  45633  elaa2  46680  smflimlem2  47218