Theorem 3adantl1 1183

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3ad2antl2  1203  3ad2antl3  1204  funcnvqp  6600  onfununi  8327  omord2  8551  en2eqpr  9990  divmuldiv  11914  ioojoin  13509  expnlbnd  14268  swrdlend  14690  2cshw  14849  lcmledvds  16656  pospropd  18380  marrepcl  22700  gsummatr01lem3  22793  upxp  23759  rnelfmlem  24088  brbtwn2  29221  wlkonprop  29972  trlsonprop  30021  pthsonprop  30059  spthonprop  30060  spthonepeq  30067  fh2  31937  homulass  32120  hoadddi  32121  hoadddir  32122  metf1o  38350  rngohomco  38569  rngoisoco  38577  op01dm  39903  paddss12  40539  wessf1ornlem  45851  elaa2  46896  smflimlem2  47434