Theorem 3adantl2 1164

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1084

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 396  df-3an 1086

This theorem is referenced by:  3ad2antl1  1182  omord2  8568  nnmord  8633  axcc3  10435  lediv2a  12112  zdiv  12636  clatleglb  18483  mulgnn0subcl  19014  mulgsubcl  19015  ghmmulg  19153  obs2ss  21624  scmatf1  22388  neiint  22963  cnpnei  23123  caublcls  25192  axlowdimlem16  28723  clwwlkext2edg  29818  ipval2lem2  30466  fh1  31380  cm2j  31382  hoadddi  31565  hoadddir  31566  lindsadd  36994  lautco  39481  sticksstones1  41523  sticksstones12  41535  supxrge  44620  infleinflem2  44653  stoweidlem44  45332  fourierdlem41  45436  fourierdlem42  45437  fourierdlem54  45448  fourierdlem83  45477  sge0uzfsumgt  45732