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  5570  omeulem1  8590  divmuldiv  12017  imasmnd2  18968  imasgrp2  19265  imasrng  20399  srgbinomlem2  20453  imasring  20560  abvdiv  21086  mdetunilem9  22935  lly1stc  23815  icccvx  25271  dchrpt  27594  dipsubdir  31450  poimirlem4  38542  fdc  38679  unichnidl  38965  dmncan1  39010  pexmidlem6N  41032  erngdvlem3  42047  erngdvlem3-rN  42055  dvalveclem  42082  dvhvaddass  42154  dvhlveclem  42165  issmflem  47736  prproropf1olem3  48586  idomcanl  49443