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

Theorem 3adantr2 1213
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
Hypothesis
Ref Expression
3adantr.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
3adantr2 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)

Proof of Theorem 3adantr2
StepHypRef Expression
1 3simpb 1051 . 2 ((𝜓𝜏𝜒) → (𝜓𝜒))
2 3adantr.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 489 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  3adant3r2  1266  po3nr  4959  funcnvqp  5848  sornom  8955  axdclem2  9198  fzadd2  12198  issubc3  16274  funcestrcsetclem9  16553  funcsetcestrclem9  16568  pgpfi  17785  imasring  18384  prdslmodd  18732  icoopnst  22473  iocopnst  22474  axcontlem4  25561  constr2pth  25893  el2wlksotot  26171  usg2wlkonot  26172  usg2wotspth  26173  nvmdi  26671  mdsl3  28361  elicc3  31283  iscringd  32766  erngdvlem3  35095  erngdvlem3-rN  35103  dvalveclem  35131  dvhlveclem  35214  dvmptfprodlem  38634  smflimlem4  39460  funcringcsetcALTV2lem9  41834  funcringcsetclem9ALTV  41857
  Copyright terms: Public domain W3C validator