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 605	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adant3r2  1202  po3nr  5578  funcnvqp  6597  sornom  10279  axdclem2  10522  fzadd2  13614  issubc3  17938  funcestrcsetclem9  18236  funcsetcestrclem9  18251  pgpfi  19732  imasrng  20312  imasring  20471  prdslmodd  21153  icoopnst  25167  iocopnst  25168  axcontlem4  29424  nvmdi  31129  mdsl3  32797  elicc3  36936  iscringd  38748  erngdvlem3  41863  erngdvlem3-rN  41871  dvalveclem  41898  dvhlveclem  41981  dvmptfprodlem  46772  smflimlem4  47602  funcringcsetcALTV2lem9  49213  funcringcsetclem9ALTV  49236