Theorem 3adantr2 1167

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  3adant3r2  1180  po3nr  5452  funcnvqp  6388  sornom  9688  axdclem2  9931  fzadd2  12937  issubc3  17111  funcestrcsetclem9  17390  funcsetcestrclem9  17405  pgpfi  18722  imasring  19365  prdslmodd  19734  icoopnst  23544  iocopnst  23545  axcontlem4  26761  nvmdi  28431  mdsl3  30099  elicc3  33778  iscringd  35436  erngdvlem3  38286  erngdvlem3-rN  38294  dvalveclem  38321  dvhlveclem  38404  dvmptfprodlem  42586  smflimlem4  43407  funcringcsetcALTV2lem9  44668  funcringcsetclem9ALTV  44691