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  6550  onfununi  8271  omord2  8492  en2eqpr  9920  divmuldiv  11843  ioojoin  13405  expnlbnd  14159  swrdlend  14579  2cshw  14738  lcmledvds  16529  pospropd  18250  marrepcl  22468  gsummatr01lem3  22561  upxp  23527  rnelfmlem  23856  brbtwn2  28869  wlkonprop  29621  trlsonprop  29670  pthsonprop  29708  spthonprop  29709  spthonepeq  29716  fh2  31582  homulass  31765  hoadddi  31766  hoadddir  31767  metf1o  37754  rngohomco  37973  rngoisoco  37981  op01dm  39181  paddss12  39818  wessf1ornlem  45183  elaa2  46235  smflimlem2  46773