Theorem 3adantr3 1190

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)

Hypothesis

Ref	Expression
3adantr.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
3adantr3	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Proof of Theorem 3adantr3

Step	Hyp	Ref	Expression
1		3simpa 1166	. 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:  3adant3r3  1203  3ad2antr1  1207  3ad2antr2  1208  sotr2  5593  dfwe2  7777  smogt  8359  infsupprpr  9482  wlogle  11830  fzadd2  13673  swrdspsleq  14795  tanadd  16315  prdssgrpd  18902  prdsmndd  18944  mhmmnd  19254  imasrng  20379  imasring  20540  prdslmodd  21224  sraassab  22156  mpllsslem  22287  scmatlss  22820  mdetunilem3  22909  ptclsg  23914  tmdgsum2  24395  isxmet2d  24626  xmetres2  24660  prdsxmetlem  24667  comet  24812  iimulcl  25238  icoopnst  25240  iocopnst  25241  icccvx  25251  dvfsumrlim  26331  dvfsumrlim2  26332  colhp  29230  eengtrkg  29546  wwlksnredwwlkn  30466  dmdsl3  32899  eqgvscpbl  33893  resconn  35980  poimirlem28  38534  poimirlem32  38538  broucube  38540  ftc1anclem7  38585  ftc1anc  38587  isdrngo2  38860  iscringd  38900  unichnidl  38933  lplnle  40565  2llnjN  40592  2lplnj  40645  osumcllem11N  40991  cdleme1  41252  erngplus2  41829  erngplus2-rN  41837  erngdvlem3  42015  erngdvlem3-rN  42023  dvaplusgv  42035  dvalveclem  42050  dvhvaddass  42122  dvhlveclem  42133  dihmeetlem12N  42343  issmflem  47681  fmtnoprmfac1  48594  lincresunit3lem2  49536  lincresunit3  49537