Theorem 3adantl2 1166

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)

Hypothesis

Ref	Expression
3adantl.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adantl2	⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem 3adantl2

Step	Hyp	Ref	Expression
1		3simpb 1148	. 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:  3ad2antl1  1184  omord2  8603  nnmord  8668  axcc3  10475  lediv2a  12159  zdiv  12685  clatleglb  18575  mulgnn0subcl  19117  mulgsubcl  19118  ghmmulg  19258  obs2ss  21766  scmatf1  22552  neiint  23127  cnpnei  23287  caublcls  25356  axlowdimlem16  28986  clwwlkext2edg  30084  ipval2lem2  30732  fh1  31646  cm2j  31648  hoadddi  31831  hoadddir  31832  lindsadd  37599  lautco  40079  sticksstones1  42127  sticksstones12  42139  supxrge  45287  infleinflem2  45320  stoweidlem44  45999  fourierdlem41  46103  fourierdlem42  46104  fourierdlem54  46115  fourierdlem83  46144  sge0uzfsumgt  46399