Theorem 3adantr1 1171

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)

Hypothesis

Ref	Expression
3adantr.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
3adantr1	⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3adantr1

Step	Hyp	Ref	Expression
1		3simpc 1151	. 2 ⊢ ((𝜏 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2		3adantr.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 594	1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3adant3r1  1184  3ad2antr3  1192  swopo  5550  omeulem1  8517  divmuldiv  11855  imasmnd2  18742  imasgrp2  19031  imasrng  20158  srgbinomlem2  20208  imasring  20310  abvdiv  20806  mdetunilem9  22585  lly1stc  23461  icccvx  24917  dchrpt  27230  dipsubdir  30919  poimirlem4  37945  fdc  38066  unichnidl  38352  dmncan1  38397  pexmidlem6N  40421  erngdvlem3  41436  erngdvlem3-rN  41444  dvalveclem  41471  dvhvaddass  41543  dvhlveclem  41554  issmflem  47155  prproropf1olem3  47965