MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3adantr3 Structured version   Visualization version   GIF version

Theorem 3adantr3 1212
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
StepHypRef Expression
1 3simpa 1178 . 2 ((𝜓𝜒𝜏) → (𝜓𝜒))
2 3adantr.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 586 1 ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  3adant3r3  1235  3ad2antr1  1239  3ad2antr2  1240  sotr2  5227  dfwe2  7179  smogt  7668  wlogle  10815  fzadd2  12583  tanadd  15181  prdsmndd  17591  mhmmnd  17806  imasring  18886  prdslmodd  19241  mpllsslem  19709  scmatlss  20608  mdetunilem3  20697  ptclsg  21698  tmdgsum2  22179  isxmet2d  22411  xmetres2  22445  prdsxmetlem  22452  comet  22597  iimulcl  23015  icoopnst  23017  iocopnst  23018  icccvx  23028  dvfsumrlim  24085  dvfsumrlim2  24086  colhp  25953  eengtrkg  26156  wwlksnredwwlkn  27095  dmdsl3  29565  resconn  31608  poimirlem28  33793  poimirlem32  33797  broucube  33799  ftc1anclem7  33846  ftc1anc  33848  isdrngo2  34111  iscringd  34151  unichnidl  34184  lplnle  35428  2llnjN  35455  2lplnj  35508  osumcllem11N  35854  cdleme1  36115  erngplus2  36692  erngplus2-rN  36700  erngdvlem3  36878  erngdvlem3-rN  36886  dvaplusgv  36898  dvalveclem  36913  dvhvaddass  36985  dvhlveclem  36996  dihmeetlem12N  37206  issmflem  41508  fmtnoprmfac1  42085  lincresunit3lem2  42870  lincresunit3  42871
  Copyright terms: Public domain W3C validator