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

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
StepHypRef Expression
1 3simpa 1149 . 2 ((𝜓𝜒𝜏) → (𝜓𝜒))
2 3adantr.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 594 1 ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  3adant3r3  1185  3ad2antr1  1189  3ad2antr2  1190  sotr2  5575  dfwe2  7699  smogt  8281  infsupprpr  9374  wlogle  11622  fzadd2  13406  swrdspsleq  14486  tanadd  15985  prdsmndd  18525  mhmmnd  18804  imasring  19974  prdslmodd  20359  mpllsslem  21334  scmatlss  21802  mdetunilem3  21891  ptclsg  22894  tmdgsum2  23375  isxmet2d  23608  xmetres2  23642  prdsxmetlem  23649  comet  23797  iimulcl  24228  icoopnst  24230  iocopnst  24231  icccvx  24241  dvfsumrlim  25323  dvfsumrlim2  25324  colhp  27517  eengtrkg  27740  wwlksnredwwlkn  28645  dmdsl3  31062  eqgvscpbl  31942  resconn  33620  poimirlem28  36037  poimirlem32  36041  broucube  36043  ftc1anclem7  36088  ftc1anc  36090  isdrngo2  36348  iscringd  36388  unichnidl  36421  lplnle  37934  2llnjN  37961  2lplnj  38014  osumcllem11N  38360  cdleme1  38621  erngplus2  39198  erngplus2-rN  39206  erngdvlem3  39384  erngdvlem3-rN  39392  dvaplusgv  39404  dvalveclem  39419  dvhvaddass  39491  dvhlveclem  39502  dihmeetlem12N  39712  issmflem  44759  fmtnoprmfac1  45548  lincresunit3lem2  46352  lincresunit3  46353
  Copyright terms: Public domain W3C validator