Theorem 3adantr2 1170

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

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

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3adant3r2  1183  po3nr  5603  funcnvqp  6612  sornom  10274  axdclem2  10517  fzadd2  13538  issubc3  17801  funcestrcsetclem9  18102  funcsetcestrclem9  18117  pgpfi  19475  imasring  20147  prdslmodd  20585  icoopnst  24462  iocopnst  24463  axcontlem4  28263  nvmdi  29939  mdsl3  31607  elicc3  35288  iscringd  36952  erngdvlem3  39947  erngdvlem3-rN  39955  dvalveclem  39982  dvhlveclem  40065  dvmptfprodlem  44739  smflimlem4  45569  imasrng  46757  funcringcsetcALTV2lem9  47021  funcringcsetclem9ALTV  47044