Theorem 3adantr3 1172

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 1148	. 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:  3adant3r3  1185  3ad2antr1  1189  3ad2antr2  1190  sotr2  5583  dfwe2  7753  smogt  8339  infsupprpr  9464  wlogle  11718  fzadd2  13527  swrdspsleq  14637  tanadd  16142  prdssgrpd  18667  prdsmndd  18704  mhmmnd  19003  imasrng  20093  imasring  20246  prdslmodd  20882  sraassab  21784  mpllsslem  21916  scmatlss  22419  mdetunilem3  22508  ptclsg  23509  tmdgsum2  23990  isxmet2d  24222  xmetres2  24256  prdsxmetlem  24263  comet  24408  iimulcl  24840  icoopnst  24843  iocopnst  24844  icccvx  24855  dvfsumrlim  25945  dvfsumrlim2  25946  colhp  28704  eengtrkg  28920  wwlksnredwwlkn  29832  dmdsl3  32251  eqgvscpbl  33328  resconn  35240  poimirlem28  37649  poimirlem32  37653  broucube  37655  ftc1anclem7  37700  ftc1anc  37702  isdrngo2  37959  iscringd  37999  unichnidl  38032  lplnle  39541  2llnjN  39568  2lplnj  39621  osumcllem11N  39967  cdleme1  40228  erngplus2  40805  erngplus2-rN  40813  erngdvlem3  40991  erngdvlem3-rN  40999  dvaplusgv  41011  dvalveclem  41026  dvhvaddass  41098  dvhlveclem  41109  dihmeetlem12N  41319  issmflem  46732  fmtnoprmfac1  47570  lincresunit3lem2  48473  lincresunit3  48474