Theorem 3adantr2 1169

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

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

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 1088

This theorem is referenced by:  3adant3r2  1182  po3nr  5518  funcnvqp  6498  sornom  10033  axdclem2  10276  fzadd2  13291  issubc3  17564  funcestrcsetclem9  17865  funcsetcestrclem9  17880  pgpfi  19210  imasring  19858  prdslmodd  20231  icoopnst  24102  iocopnst  24103  axcontlem4  27335  nvmdi  29010  mdsl3  30678  elicc3  34506  iscringd  36156  erngdvlem3  39004  erngdvlem3-rN  39012  dvalveclem  39039  dvhlveclem  39122  dvmptfprodlem  43485  smflimlem4  44309  funcringcsetcALTV2lem9  45602  funcringcsetclem9ALTV  45625