Theorem 3adantl1 1185

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

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

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 1105

This theorem is referenced by:  3ad2antl2  1205  3ad2antl3  1206  funcnvqp  6600  onfununi  8324  omord2  8548  en2eqpr  9987  divmuldiv  11910  ioojoin  13505  expnlbnd  14265  swrdlend  14687  2cshw  14846  lcmledvds  16652  pospropd  18376  marrepcl  22721  gsummatr01lem3  22814  upxp  23780  rnelfmlem  24109  brbtwn2  29255  wlkonprop  30006  trlsonprop  30055  pthsonprop  30093  spthonprop  30094  spthonepeq  30101  fh2  31971  homulass  32154  hoadddi  32155  hoadddir  32156  ltnmul  36693  metf1o  38406  rngohomco  38625  rngoisoco  38633  op01dm  39957  paddss12  40593  wessf1ornlem  45903  elaa2  46948  smflimlem2  47486