Theorem 3adantr2 1214

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)

Hypothesis

Ref	Expression
3adantr.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
3adantr2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3adantr2

Step	Hyp	Ref	Expression
1		3simpb 1052	. 2 ⊢ ((𝜓 ∧ 𝜏 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2		3adantr.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 490	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3adant3r2  1267  po3nr  4973  funcnvqp  5866  sornom  8982  axdclem2  9225  fzadd2  12247  issubc3  16332  funcestrcsetclem9  16611  funcsetcestrclem9  16626  pgpfi  17843  imasring  18442  prdslmodd  18790  icoopnst  22546  iocopnst  22547  axcontlem4  25647  constr2pth  26131  el2wlksotot  26409  usg2wlkonot  26410  usg2wotspth  26411  nvmdi  26887  mdsl3  28559  elicc3  31481  iscringd  32967  erngdvlem3  35296  erngdvlem3-rN  35304  dvalveclem  35332  dvhlveclem  35415  dvmptfprodlem  38834  smflimlem4  39660  funcringcsetcALTV2lem9  41836  funcringcsetclem9ALTV  41859