Theorem 3adantl2 1163

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3ad2antl1  1181  omord2  8195  nnmord  8260  axcc3  9862  lediv2a  11536  zdiv  12055  clatleglb  17738  mulgnn0subcl  18243  mulgsubcl  18244  ghmmulg  18372  obs2ss  20875  scmatf1  21142  neiint  21714  cnpnei  21874  caublcls  23914  axlowdimlem16  26745  clwwlkext2edg  27837  ipval2lem2  28483  fh1  29397  cm2j  29399  hoadddi  29582  hoadddir  29583  lindsadd  34887  lautco  37235  supxrge  41613  infleinflem2  41646  stoweidlem44  42336  fourierdlem41  42440  fourierdlem42  42441  fourierdlem54  42452  fourierdlem83  42481  sge0uzfsumgt  42733