Theorem 3adantr2 1171

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 1149	. 2 ⊢ ((𝜓 ∧ 𝜏 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2		3adantr.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 593	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

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

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

This theorem is referenced by:  3adant3r2  1184  po3nr  5534  funcnvqp  6540  sornom  10163  axdclem2  10406  fzadd2  13454  issubc3  17751  funcestrcsetclem9  18049  funcsetcestrclem9  18064  pgpfi  19512  imasrng  20090  imasring  20243  prdslmodd  20897  icoopnst  24858  iocopnst  24859  axcontlem4  28940  nvmdi  30620  mdsl3  32288  elicc3  36351  iscringd  38038  erngdvlem3  41029  erngdvlem3-rN  41037  dvalveclem  41064  dvhlveclem  41147  dvmptfprodlem  45982  smflimlem4  46812  funcringcsetcALTV2lem9  48329  funcringcsetclem9ALTV  48352