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

Theorem 3adantr3 1168
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 1145 . 2 ((𝜓𝜒𝜏) → (𝜓𝜒))
2 3adantr.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 595 1 ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 400  df-3an 1086
This theorem is referenced by:  3adant3r3  1181  3ad2antr1  1185  3ad2antr2  1186  sotr2  5478  dfwe2  7471  smogt  7979  infsupprpr  8944  wlogle  11150  fzadd2  12925  swrdspsleq  14006  tanadd  15499  prdsmndd  17923  mhmmnd  18200  imasring  19348  prdslmodd  19717  mpllsslem  20191  scmatlss  21110  mdetunilem3  21199  ptclsg  22199  tmdgsum2  22680  isxmet2d  22913  xmetres2  22947  prdsxmetlem  22954  comet  23099  iimulcl  23521  icoopnst  23523  iocopnst  23524  icccvx  23534  dvfsumrlim  24613  dvfsumrlim2  24614  colhp  26543  eengtrkg  26759  wwlksnredwwlkn  27660  dmdsl3  30077  eqgvscpbl  30927  resconn  32501  poimirlem28  34971  poimirlem32  34975  broucube  34977  ftc1anclem7  35022  ftc1anc  35024  isdrngo2  35282  iscringd  35322  unichnidl  35355  lplnle  36722  2llnjN  36749  2lplnj  36802  osumcllem11N  37148  cdleme1  37409  erngplus2  37986  erngplus2-rN  37994  erngdvlem3  38172  erngdvlem3-rN  38180  dvaplusgv  38192  dvalveclem  38207  dvhvaddass  38279  dvhlveclem  38290  dihmeetlem12N  38500  issmflem  43184  fmtnoprmfac1  43905  lincresunit3lem2  44711  lincresunit3  44712
  Copyright terms: Public domain W3C validator