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

Theorem 3anidm13 1533
Description: Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
Hypothesis
Ref Expression
3anidm13.1 ((𝜑𝜓𝜑) → 𝜒)
Assertion
Ref Expression
3anidm13 ((𝜑𝜓) → 𝜒)

Proof of Theorem 3anidm13
StepHypRef Expression
1 3anidm13.1 . . 3 ((𝜑𝜓𝜑) → 𝜒)
213com23 1147 . 2 ((𝜑𝜑𝜓) → 𝜒)
323anidm12 1532 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1098
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 198  df-an 384  df-3an 1100
This theorem is referenced by:  npncan2  10531  ltsubpos  10743  leaddle0  10766  subge02  10767  halfaddsub  11489  avglt1  11494  hashssdif  13424  pythagtriplem4  15751  pythagtriplem14  15760  lsmss2  18308  grpoidinvlem2  27716  hvpncan3  28256  bcm1n  29911  3anidm12p1  39570  3impcombi  39581
  Copyright terms: Public domain W3C validator