Theorem 3adantl2 1168

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 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  1186  omord2  8494  nnmord  8560  axcc3  10348  lediv2a  12036  zdiv  12562  clatleglb  18441  mulgnn0subcl  19017  mulgsubcl  19018  ghmmulg  19157  obs2ss  21684  scmatf1  22475  neiint  23048  cnpnei  23208  caublcls  25265  axlowdimlem16  29030  clwwlkext2edg  30131  ipval2lem2  30779  fh1  31693  cm2j  31695  hoadddi  31878  hoadddir  31879  lindsadd  37810  lautco  40353  sticksstones1  42396  sticksstones12  42408  supxrge  45579  infleinflem2  45611  stoweidlem44  46284  fourierdlem41  46388  fourierdlem42  46389  fourierdlem54  46400  fourierdlem83  46429  sge0uzfsumgt  46684