Theorem 3adantr2 1165

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1082

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 209  df-an 399  df-3an 1084

This theorem is referenced by:  3adant3r2  1178  po3nr  5481  funcnvqp  6411  sornom  9692  axdclem2  9935  fzadd2  12939  issubc3  17114  funcestrcsetclem9  17393  funcsetcestrclem9  17408  pgpfi  18725  imasring  19364  prdslmodd  19736  icoopnst  23538  iocopnst  23539  axcontlem4  26751  nvmdi  28423  mdsl3  30091  elicc3  33686  iscringd  35309  erngdvlem3  38159  erngdvlem3-rN  38167  dvalveclem  38194  dvhlveclem  38277  dvmptfprodlem  42303  smflimlem4  43124  funcringcsetcALTV2lem9  44389  funcringcsetclem9ALTV  44412