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

Syntax hints:   → wi 4   ∧ wa 394   ∧ 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 395  df-3an 1086

This theorem is referenced by:  3ad2antl1  1182  omord2  8596  nnmord  8661  axcc3  10471  lediv2a  12148  zdiv  12672  clatleglb  18519  mulgnn0subcl  19056  mulgsubcl  19057  ghmmulg  19196  obs2ss  21677  scmatf1  22461  neiint  23036  cnpnei  23196  caublcls  25265  axlowdimlem16  28796  clwwlkext2edg  29894  ipval2lem2  30542  fh1  31456  cm2j  31458  hoadddi  31641  hoadddir  31642  lindsadd  37127  lautco  39610  sticksstones1  41658  sticksstones12  41670  supxrge  44767  infleinflem2  44800  stoweidlem44  45479  fourierdlem41  45583  fourierdlem42  45584  fourierdlem54  45595  fourierdlem83  45624  sge0uzfsumgt  45879