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

Theorem 3anidm23 1418
Description: Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.)
Hypothesis
Ref Expression
3anidm23.1 ((𝜑𝜓𝜓) → 𝜒)
Assertion
Ref Expression
3anidm23 ((𝜑𝜓) → 𝜒)

Proof of Theorem 3anidm23
StepHypRef Expression
1 3anidm23.1 . . 3 ((𝜑𝜓𝜓) → 𝜒)
213expa 1115 . 2 (((𝜑𝜓) ∧ 𝜓) → 𝜒)
32anabss3 673 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  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 206  df-an 395  df-3an 1086
This theorem is referenced by:  supsn  9497  infsn  9530  grusn  10829  subeq0  11518  halfaddsub  12478  avglt2  12484  modabs2  13906  efsub  16080  sinmul  16152  divalgmod  16386  modgcd  16511  prmdvdssqOLD  16693  pythagtriplem4  16791  pythagtriplem16  16802  pltirr  18330  latjidm  18457  latmidm  18469  ipopos  18531  mulgmodid  19076  f1omvdcnv  19411  lsmss1  19632  rhmsubclem3  20632  zntoslem  21507  obsipid  21673  smadiadetlem2  22610  smadiadet  22616  ordtt1  23327  xmet0  24292  nmsq  25166  tcphcphlem3  25205  tcphcph  25209  grpoidinvlem1  30386  grpodivid  30424  nvmid  30541  ipidsq  30592  5oalem1  31536  3oalem2  31545  unopf1o  31798  unopnorm  31799  hmopre  31805  ballotlemfc0  34243  ballotlemfcc  34244  gcdabsorb  35475  cgr3rflx  35781  endofsegid  35812  tailini  35991  nnssi2  36070  nndivlub  36073  brin2  38011  opoccl  38796  opococ  38797  opexmid  38809  opnoncon  38810  cmtidN  38859  ltrniotaidvalN  40186  pell14qrexpclnn0  42428  rmxdbl  42502  rmydbl  42503  rhmsubcALTVlem3  47531
  Copyright terms: Public domain W3C validator