Theorem 3adantl2 1186

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3ad2antl1  1204  omord2  8558  nnmord  8624  axcc3  10444  lediv2a  12137  zdiv  12695  clatleglb  18612  mulgnn0subcl  19216  mulgsubcl  19217  ghmmulg  19361  obs2ss  21948  scmatf1  22759  neiint  23335  cnpnei  23495  caublcls  25543  axlowdimlem16  29422  clwwlkext2edg  30534  ipval2lem2  31193  fh1  32107  cm2j  32109  hoadddi  32292  hoadddir  32293  lindsadd  38375  lautco  40978  sticksstones1  43020  sticksstones12  43032  supxrge  46176  infleinflem2  46208  stoweidlem44  46880  fourierdlem41  46984  fourierdlem42  46985  fourierdlem54  46996  fourierdlem83  47025  sge0uzfsumgt  47280