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  5595  dfwe2  7766  smogt  8379  infsupprpr  9516  wlogle  11768  fzadd2  13574  swrdspsleq  14681  tanadd  16183  prdssgrpd  18709  prdsmndd  18746  mhmmnd  19045  imasrng  20135  imasring  20288  prdslmodd  20924  sraassab  21826  mpllsslem  21958  scmatlss  22461  mdetunilem3  22550  ptclsg  23551  tmdgsum2  24032  isxmet2d  24264  xmetres2  24298  prdsxmetlem  24305  comet  24450  iimulcl  24882  icoopnst  24885  iocopnst  24886  icccvx  24897  dvfsumrlim  25988  dvfsumrlim2  25989  colhp  28695  eengtrkg  28911  wwlksnredwwlkn  29823  dmdsl3  32242  eqgvscpbl  33311  resconn  35214  poimirlem28  37618  poimirlem32  37622  broucube  37624  ftc1anclem7  37669  ftc1anc  37671  isdrngo2  37928  iscringd  37968  unichnidl  38001  lplnle  39505  2llnjN  39532  2lplnj  39585  osumcllem11N  39931  cdleme1  40192  erngplus2  40769  erngplus2-rN  40777  erngdvlem3  40955  erngdvlem3-rN  40963  dvaplusgv  40975  dvalveclem  40990  dvhvaddass  41062  dvhlveclem  41073  dihmeetlem12N  41283  issmflem  46704  fmtnoprmfac1  47527  lincresunit3lem2  48404  lincresunit3  48405