Theorem 3adantl2 1165

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  3ad2antl1  1183  omord2  8569  nnmord  8634  axcc3  10435  lediv2a  12112  zdiv  12636  clatleglb  18475  mulgnn0subcl  19003  mulgsubcl  19004  ghmmulg  19142  obs2ss  21503  scmatf1  22253  neiint  22828  cnpnei  22988  caublcls  25057  axlowdimlem16  28482  clwwlkext2edg  29576  ipval2lem2  30224  fh1  31138  cm2j  31140  hoadddi  31323  hoadddir  31324  lindsadd  36784  lautco  39271  sticksstones1  41268  sticksstones12  41280  supxrge  44346  infleinflem2  44379  stoweidlem44  45058  fourierdlem41  45162  fourierdlem42  45163  fourierdlem54  45174  fourierdlem83  45203  sge0uzfsumgt  45458