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

Theorem 3anidm13 1417
 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 1123 . 2 ((𝜑𝜑𝜓) → 𝜒)
323anidm12 1416 1 ((𝜑𝜓) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  npncan2  10904  ltsubpos  11123  leaddle0  11146  subge02  11147  halfaddsub  11860  avglt1  11865  hashssdif  13771  pythagtriplem4  16148  pythagtriplem14  16157  lsmss2  18788  grpoidinvlem2  28295  hvpncan3  28832  bcm1n  30551  revpfxsfxrev  32487  nnproddivdvdsd  39305  resubidaddid1  39548  reposdif  39594  3anidm12p1  41527  3impcombi  41538
 Copyright terms: Public domain W3C validator