Theorem 3adantr1 1188

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adant3r1  1201  3ad2antr3  1209  swopo  5577  omeulem1  8628  divmuldiv  12057  imasmnd2  19018  imasgrp2  19315  imasrng  20450  srgbinomlem2  20504  imasring  20611  abvdiv  21137  mdetunilem9  22990  lly1stc  23870  icccvx  25326  dchrpt  27651  dipsubdir  31507  poimirlem4  38810  fdc  38945  unichnidl  39231  dmncan1  39276  pexmidlem6N  41298  erngdvlem3  42313  erngdvlem3-rN  42321  dvalveclem  42348  dvhvaddass  42420  dvhlveclem  42431  issmflem  48010  prproropf1olem3  48860  idomcanl  49775