Theorem 3adantr1 1213

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

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

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3ad2antr3  1221  3adant3r1  1266  swopo  4969  omeulem1  7549  divmuldiv  10604  imasmnd2  17150  imasgrp2  17353  srgbinomlem2  18364  imasring  18442  abvdiv  18660  mdetunilem9  20245  lly1stc  21109  icccvx  22557  dchrpt  24792  dipsubdir  27087  poimirlem4  32583  fdc  32711  unichnidl  33000  dmncan1  33045  pexmidlem6N  34279  erngdvlem3  35296  erngdvlem3-rN  35304  dvalveclem  35332  dvhvaddass  35404  dvhlveclem  35415  issmflem  39613