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 604	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3adant3r3  1203  3ad2antr1  1207  3ad2antr2  1208  sotr2  5605  dfwe2  7774  smogt  8355  infsupprpr  9467  wlogle  11748  fzadd2  13589  swrdspsleq  14705  tanadd  16224  prdssgrpd  18792  prdsmndd  18829  mhmmnd  19131  imasrng  20256  imasring  20413  prdslmodd  21071  sraassab  21999  mpllsslem  22130  scmatlss  22663  mdetunilem3  22752  ptclsg  23753  tmdgsum2  24234  isxmet2d  24465  xmetres2  24499  prdsxmetlem  24506  comet  24651  iimulcl  25077  icoopnst  25079  iocopnst  25080  icccvx  25090  dvfsumrlim  26171  dvfsumrlim2  26172  colhp  29033  eengtrkg  29317  wwlksnredwwlkn  30225  dmdsl3  32648  eqgvscpbl  33651  resconn  35719  poimirlem28  38280  poimirlem32  38284  broucube  38286  ftc1anclem7  38331  ftc1anc  38333  isdrngo2  38590  iscringd  38630  unichnidl  38663  lplnle  40295  2llnjN  40322  2lplnj  40375  osumcllem11N  40721  cdleme1  40982  erngplus2  41559  erngplus2-rN  41567  erngdvlem3  41745  erngdvlem3-rN  41753  dvaplusgv  41765  dvalveclem  41780  dvhvaddass  41852  dvhlveclem  41863  dihmeetlem12N  42073  issmflem  47424  fmtnoprmfac1  48300  lincresunit3lem2  49243  lincresunit3  49244