Theorem 3adantr2 1177

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3adant3r2  1190  po3nr  5541  funcnvqp  6549  sornom  10190  axdclem2  10433  fzadd2  13504  issubc3  17807  funcestrcsetclem9  18105  funcsetcestrclem9  18120  pgpfi  19571  imasrng  20149  imasring  20301  prdslmodd  20959  icoopnst  24924  iocopnst  24925  axcontlem4  29054  nvmdi  30737  mdsl3  32405  elicc3  36545  iscringd  38365  erngdvlem3  41482  erngdvlem3-rN  41490  dvalveclem  41517  dvhlveclem  41600  dvmptfprodlem  46387  smflimlem4  47217  funcringcsetcALTV2lem9  48789  funcringcsetclem9ALTV  48812