Theorem 3adantl2 1167

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 1089

This theorem is referenced by:  3ad2antl1  1185  omord2  8519  nnmord  8584  axcc3  10383  lediv2a  12058  zdiv  12582  clatleglb  18421  mulgnn0subcl  18903  mulgsubcl  18904  ghmmulg  19034  obs2ss  21172  scmatf1  21917  neiint  22492  cnpnei  22652  caublcls  24710  axlowdimlem16  27969  clwwlkext2edg  29063  ipval2lem2  29709  fh1  30623  cm2j  30625  hoadddi  30808  hoadddir  30809  lindsadd  36144  lautco  38633  sticksstones1  40627  sticksstones12  40639  supxrge  43693  infleinflem2  43726  stoweidlem44  44405  fourierdlem41  44509  fourierdlem42  44510  fourierdlem54  44521  fourierdlem83  44550  sge0uzfsumgt  44805