Theorem 3adantr2 1169

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 1148	. 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  1182  po3nr  5611  funcnvqp  6631  sornom  10314  axdclem2  10557  fzadd2  13595  issubc3  17899  funcestrcsetclem9  18203  funcsetcestrclem9  18218  pgpfi  19637  imasrng  20194  imasring  20343  prdslmodd  20984  icoopnst  24982  iocopnst  24983  axcontlem4  28996  nvmdi  30676  mdsl3  32344  elicc3  36299  iscringd  37984  erngdvlem3  40972  erngdvlem3-rN  40980  dvalveclem  41007  dvhlveclem  41090  dvmptfprodlem  45899  smflimlem4  46729  funcringcsetcALTV2lem9  48141  funcringcsetclem9ALTV  48164