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 591	1 ⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3ad2antl1  1204  omord2  8553  nnmord  8619  axcc3  10423  lediv2a  12110  zdiv  12667  clatleglb  18575  mulgnn0subcl  19154  mulgsubcl  19155  ghmmulg  19299  obs2ss  21860  scmatf1  22669  neiint  23242  cnpnei  23402  caublcls  25449  axlowdimlem16  29285  clwwlkext2edg  30385  ipval2lem2  31034  fh1  31948  cm2j  31950  hoadddi  32133  hoadddir  32134  lindsadd  38242  lautco  40849  sticksstones1  42891  sticksstones12  42903  supxrge  46034  infleinflem2  46066  stoweidlem44  46738  fourierdlem41  46842  fourierdlem42  46843  fourierdlem54  46854  fourierdlem83  46883  sge0uzfsumgt  47138