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

Theorem 3anidm13 1376
 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 1263 . 2 ((𝜑𝜑𝜓) → 𝜒)
323anidm12 1375 1 ((𝜑𝜓) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  npncan2  10187  ltsubpos  10399  leaddle0  10422  subge02  10423  halfaddsub  11142  avglt1  11147  hashssdif  13061  pythagtriplem4  15362  pythagtriplem14  15371  lsmss2  17904  grpoidinvlem2  26743  hvpncan3  27283  bcm1n  28941  fv1stcnv  30925  sltasym  31071  3anidm12p1  38054  3impcombi  38065
 Copyright terms: Public domain W3C validator