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 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:  3ad2antl1  1184  omord2  8398  nnmord  8463  axcc3  10194  lediv2a  11869  zdiv  12390  clatleglb  18236  mulgnn0subcl  18717  mulgsubcl  18718  ghmmulg  18846  obs2ss  20936  scmatf1  21680  neiint  22255  cnpnei  22415  caublcls  24473  axlowdimlem16  27325  clwwlkext2edg  28420  ipval2lem2  29066  fh1  29980  cm2j  29982  hoadddi  30165  hoadddir  30166  lindsadd  35770  lautco  38111  sticksstones1  40102  sticksstones12  40114  supxrge  42877  infleinflem2  42910  stoweidlem44  43585  fourierdlem41  43689  fourierdlem42  43690  fourierdlem54  43701  fourierdlem83  43730  sge0uzfsumgt  43982