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

Theorem 3anidm13 1424
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 1291 . 2 ((𝜑𝜑𝜓) → 𝜒)
323anidm12 1423 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  npncan2  10346  ltsubpos  10558  leaddle0  10581  subge02  10582  halfaddsub  11303  avglt1  11308  hashssdif  13238  pythagtriplem4  15571  pythagtriplem14  15580  lsmss2  18127  grpoidinvlem2  27487  hvpncan3  28027  bcm1n  29682  3anidm12p1  39350  3impcombi  39361
  Copyright terms: Public domain W3C validator