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  8603  nnmord  8669  axcc3  10543  lediv2a  12238  zdiv  12796  clatleglb  18721  mulgnn0subcl  19326  mulgsubcl  19327  ghmmulg  19471  obs2ss  22065  scmatf1  22876  neiint  23452  cnpnei  23612  caublcls  25660  axlowdimlem16  29565  clwwlkext2edg  30677  ipval2lem2  31336  fh1  32250  cm2j  32252  hoadddi  32435  hoadddir  32436  lindsadd  38728  lautco  41346  sticksstones1  43388  sticksstones12  43400  supxrge  46555  infleinflem2  46587  stoweidlem44  47259  fourierdlem41  47363  fourierdlem42  47364  fourierdlem54  47375  fourierdlem83  47404  sge0uzfsumgt  47659