Theorem 3adantr2 1176

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  3adant3r2  1199  po3nr  5201  funcnvqp  6113  sornom  9311  axdclem2  9554  fzadd2  12589  issubc3  16730  funcestrcsetclem9  17009  funcsetcestrclem9  17024  pgpfi  18240  imasring  18839  prdslmodd  19191  icoopnst  22959  iocopnst  22960  axcontlem4  26067  nvmdi  27833  mdsl3  29505  elicc3  32638  iscringd  34128  erngdvlem3  36798  erngdvlem3-rN  36806  dvalveclem  36834  dvhlveclem  36917  dvmptfprodlem  40680  smflimlem4  41506  funcringcsetcALTV2lem9  42572  funcringcsetclem9ALTV  42595