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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3ad2antl1  1204  omord2  8578  nnmord  8644  axcc3  10519  lediv2a  12214  zdiv  12772  clatleglb  18697  mulgnn0subcl  19302  mulgsubcl  19303  ghmmulg  19447  obs2ss  22040  scmatf1  22851  neiint  23427  cnpnei  23587  caublcls  25635  axlowdimlem16  29540  clwwlkext2edg  30652  ipval2lem2  31311  fh1  32225  cm2j  32227  hoadddi  32410  hoadddir  32411  lindsadd  38629  lautco  41247  sticksstones1  43289  sticksstones12  43301  supxrge  46443  infleinflem2  46475  stoweidlem44  47147  fourierdlem41  47251  fourierdlem42  47252  fourierdlem54  47263  fourierdlem83  47292  sge0uzfsumgt  47547