Theorem 3adantl1 1163

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  3ad2antl2  1183  3ad2antl3  1184  funcnvqp  6615  onfununi  8363  omord2  8589  en2eqpr  10043  divmuldiv  11959  ioojoin  13508  expnlbnd  14245  swrdlend  14656  2cshw  14816  lcmledvds  16595  pospropd  18347  marrepcl  22554  gsummatr01lem3  22647  upxp  23615  rnelfmlem  23944  brbtwn2  28836  wlkonprop  29592  trlsonprop  29642  pthsonprop  29678  spthonprop  29679  spthonepeq  29686  fh2  31549  homulass  31732  hoadddi  31733  hoadddir  31734  metf1o  37469  rngohomco  37688  rngoisoco  37696  op01dm  38894  paddss12  39531  wessf1ornlem  44828  elaa2  45891  smflimlem2  46429