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

Theorem 3anidm13 1412
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 1118 . 2 ((𝜑𝜑𝜓) → 𝜒)
323anidm12 1411 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:  npncan2  10901  ltsubpos  11120  leaddle0  11143  subge02  11144  halfaddsub  11858  avglt1  11863  hashssdif  13761  pythagtriplem4  16144  pythagtriplem14  16153  lsmss2  18722  grpoidinvlem2  28209  hvpncan3  28746  bcm1n  30444  revpfxsfxrev  32259  resubidaddid1  39103  3anidm12p1  41017  3impcombi  41028
  Copyright terms: Public domain W3C validator