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

Theorem 3anidm23 1413
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 1110 . 2 (((𝜑𝜓) ∧ 𝜓) → 𝜒)
32anabss3 671 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  supsn  8924  infsn  8957  grusn  10214  subeq0  10900  halfaddsub  11858  avglt2  11864  modabs2  13261  efsub  15441  sinmul  15513  divalgmod  15745  modgcd  15868  pythagtriplem4  16144  pythagtriplem16  16155  pltirr  17561  latjidm  17672  latmidm  17684  ipopos  17758  mulgmodid  18204  f1omvdcnv  18501  lsmss1  18720  zntoslem  20631  obsipid  20794  smadiadetlem2  21201  smadiadet  21207  ordtt1  21915  xmet0  22879  nmsq  23725  tcphcphlem3  23763  tcphcph  23767  grpoidinvlem1  28208  grpodivid  28246  nvmid  28363  ipidsq  28414  5oalem1  29358  3oalem2  29367  unopf1o  29620  unopnorm  29621  hmopre  29627  ballotlemfc0  31649  ballotlemfcc  31650  pdivsq  32878  gcdabsorb  32881  cgr3rflx  33412  endofsegid  33443  tailini  33621  nnssi2  33700  nndivlub  33703  brin2  35537  opoccl  36210  opococ  36211  opexmid  36223  opnoncon  36224  cmtidN  36273  ltrniotaidvalN  37599  pell14qrexpclnn0  39341  rmxdbl  39414  rmydbl  39415  rhmsubclem3  44287  rhmsubcALTVlem3  44305
  Copyright terms: Public domain W3C validator