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 1149	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜒))
2		3adantr.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 593	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3adant3r3  1185  3ad2antr1  1189  3ad2antr2  1190  sotr2  5626  dfwe2  7794  smogt  8407  infsupprpr  9544  wlogle  11796  fzadd2  13599  swrdspsleq  14703  tanadd  16203  prdssgrpd  18746  prdsmndd  18783  mhmmnd  19082  imasrng  20174  imasring  20327  prdslmodd  20967  sraassab  21888  mpllsslem  22020  scmatlss  22531  mdetunilem3  22620  ptclsg  23623  tmdgsum2  24104  isxmet2d  24337  xmetres2  24371  prdsxmetlem  24378  comet  24526  iimulcl  24966  icoopnst  24969  iocopnst  24970  icccvx  24981  dvfsumrlim  26072  dvfsumrlim2  26073  colhp  28778  eengtrkg  29001  wwlksnredwwlkn  29915  dmdsl3  32334  eqgvscpbl  33378  resconn  35251  poimirlem28  37655  poimirlem32  37659  broucube  37661  ftc1anclem7  37706  ftc1anc  37708  isdrngo2  37965  iscringd  38005  unichnidl  38038  lplnle  39542  2llnjN  39569  2lplnj  39622  osumcllem11N  39968  cdleme1  40229  erngplus2  40806  erngplus2-rN  40814  erngdvlem3  40992  erngdvlem3-rN  41000  dvaplusgv  41012  dvalveclem  41027  dvhvaddass  41099  dvhlveclem  41110  dihmeetlem12N  41320  issmflem  46742  fmtnoprmfac1  47552  lincresunit3lem2  48397  lincresunit3  48398