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  6564  onfununi  8287  omord2  8508  en2eqpr  9936  divmuldiv  11858  ioojoin  13420  expnlbnd  14174  swrdlend  14594  2cshw  14754  lcmledvds  16545  pospropd  18262  marrepcl  22427  gsummatr01lem3  22520  upxp  23486  rnelfmlem  23815  brbtwn2  28808  wlkonprop  29560  trlsonprop  29609  pthsonprop  29647  spthonprop  29648  spthonepeq  29655  fh2  31521  homulass  31704  hoadddi  31705  hoadddir  31706  metf1o  37722  rngohomco  37941  rngoisoco  37949  op01dm  39149  paddss12  39786  wessf1ornlem  45152  elaa2  46205  smflimlem2  46743