Theorem 3adantr1 1168

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  3adant3r1  1181  3ad2antr3  1189  swopo  5607  omeulem1  8618  divmuldiv  11964  imasmnd2  18799  imasgrp2  19085  imasrng  20194  srgbinomlem2  20244  imasring  20343  abvdiv  20846  mdetunilem9  22641  lly1stc  23519  icccvx  24994  dchrpt  27325  dipsubdir  30876  poimirlem4  37610  fdc  37731  unichnidl  38017  dmncan1  38062  pexmidlem6N  39957  erngdvlem3  40972  erngdvlem3-rN  40980  dvalveclem  41007  dvhvaddass  41079  dvhlveclem  41090  issmflem  46682  prproropf1olem3  47429