Theorem 3adantr1 1170

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 1150	. 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  1183  3ad2antr3  1191  swopo  5530  omeulem1  8492  divmuldiv  11816  imasmnd2  18677  imasgrp2  18963  imasrng  20090  srgbinomlem2  20140  imasring  20243  abvdiv  20739  mdetunilem9  22530  lly1stc  23406  icccvx  24870  dchrpt  27200  dipsubdir  30820  poimirlem4  37664  fdc  37785  unichnidl  38071  dmncan1  38116  pexmidlem6N  40014  erngdvlem3  41029  erngdvlem3-rN  41037  dvalveclem  41064  dvhvaddass  41136  dvhlveclem  41147  issmflem  46765  prproropf1olem3  47536