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  8492  nnmord  8557  axcc3  10351  lediv2a  12037  zdiv  12564  clatleglb  18442  mulgnn0subcl  18984  mulgsubcl  18985  ghmmulg  19125  obs2ss  21654  scmatf1  22434  neiint  23007  cnpnei  23167  caublcls  25225  axlowdimlem16  28920  clwwlkext2edg  30018  ipval2lem2  30666  fh1  31580  cm2j  31582  hoadddi  31765  hoadddir  31766  lindsadd  37592  lautco  40076  sticksstones1  42119  sticksstones12  42131  supxrge  45318  infleinflem2  45351  stoweidlem44  46026  fourierdlem41  46130  fourierdlem42  46131  fourierdlem54  46142  fourierdlem83  46171  sge0uzfsumgt  46426