Theorem 3adantl2 1184

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

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

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 1103

This theorem is referenced by:  3ad2antl1  1202  omord2  8548  nnmord  8614  axcc3  10418  lediv2a  12105  zdiv  12662  clatleglb  18570  mulgnn0subcl  19149  mulgsubcl  19150  ghmmulg  19294  obs2ss  21844  scmatf1  22653  neiint  23226  cnpnei  23386  caublcls  25433  axlowdimlem16  29244  clwwlkext2edg  30344  ipval2lem2  30993  fh1  31907  cm2j  31909  hoadddi  32092  hoadddir  32093  lindsadd  38147  lautco  40756  sticksstones1  42798  sticksstones12  42810  supxrge  45941  infleinflem2  45973  stoweidlem44  46645  fourierdlem41  46749  fourierdlem42  46750  fourierdlem54  46761  fourierdlem83  46790  sge0uzfsumgt  47045