Theorem 3adantl1 1165

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3ad2antl2  1185  3ad2antl3  1186  funcnvqp  6498  onfununi  8172  omord2  8398  en2eqpr  9763  divmuldiv  11675  ioojoin  13215  expnlbnd  13948  swrdlend  14366  2cshw  14526  lcmledvds  16304  pospropd  18045  marrepcl  21713  gsummatr01lem3  21806  upxp  22774  rnelfmlem  23103  brbtwn2  27273  wlkonprop  28026  trlsonprop  28076  pthsonprop  28112  spthonprop  28113  spthonepeq  28120  fh2  29981  homulass  30164  hoadddi  30165  hoadddir  30166  metf1o  35913  rngohomco  36132  rngoisoco  36140  op01dm  37197  paddss12  37833  wessf1ornlem  42722  elaa2  43775  smflimlem2  44307