Theorem 3adantr2 1187

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

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

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 1103

This theorem is referenced by:  3adant3r2  1200  po3nr  5582  funcnvqp  6597  sornom  10257  axdclem2  10500  fzadd2  13583  issubc3  17902  funcestrcsetclem9  18200  funcsetcestrclem9  18215  pgpfi  19671  imasrng  20251  imasring  20408  prdslmodd  21064  icoopnst  25063  iocopnst  25064  axcontlem4  29254  nvmdi  30937  mdsl3  32605  elicc3  36713  iscringd  38532  erngdvlem3  41649  erngdvlem3-rN  41657  dvalveclem  41684  dvhlveclem  41767  dvmptfprodlem  46543  smflimlem4  47373  funcringcsetcALTV2lem9  48945  funcringcsetclem9ALTV  48968