Theorem 3adantr2 1189

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

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

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 1105

This theorem is referenced by:  3adant3r2  1202  po3nr  5586  funcnvqp  6602  sornom  10262  axdclem2  10505  fzadd2  13589  issubc3  17907  funcestrcsetclem9  18205  funcsetcestrclem9  18220  pgpfi  19676  imasrng  20256  imasring  20413  prdslmodd  21071  icoopnst  25079  iocopnst  25080  axcontlem4  29298  nvmdi  30981  mdsl3  32649  elicc3  36809  iscringd  38630  erngdvlem3  41745  erngdvlem3-rN  41753  dvalveclem  41780  dvhlveclem  41863  dvmptfprodlem  46641  smflimlem4  47471  funcringcsetcALTV2lem9  49046  funcringcsetclem9ALTV  49069