Theorem 3adantl1 1173

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3ad2antl2  1193  3ad2antl3  1194  funcnvqp  6549  onfununi  8271  omord2  8492  en2eqpr  9920  divmuldiv  11846  ioojoin  13427  expnlbnd  14186  swrdlend  14607  2cshw  14766  lcmledvds  16559  pospropd  18282  marrepcl  22547  gsummatr01lem3  22640  upxp  23606  rnelfmlem  23935  brbtwn2  28992  wlkonprop  29743  trlsonprop  29792  pthsonprop  29830  spthonprop  29831  spthonepeq  29838  fh2  31708  homulass  31891  hoadddi  31892  hoadddir  31893  metf1o  38122  rngohomco  38341  rngoisoco  38349  op01dm  39675  paddss12  40311  wessf1ornlem  45632  elaa2  46677  smflimlem2  47215