Theorem 3adantr1 1175

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 1147	. 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:  3adant3r1  1198  3ad2antr3  1206  swopo  5195  omeulem1  7829  divmuldiv  10915  imasmnd2  17526  imasgrp2  17729  srgbinomlem2  18739  imasring  18817  abvdiv  19037  mdetunilem9  20626  lly1stc  21499  icccvx  22948  dchrpt  25189  dipsubdir  28010  poimirlem4  33724  fdc  33852  unichnidl  34141  dmncan1  34186  pexmidlem6N  35762  erngdvlem3  36778  erngdvlem3-rN  36786  dvalveclem  36814  dvhvaddass  36886  dvhlveclem  36897  issmflem  41440