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

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

Proof of Theorem 3anidm12
StepHypRef Expression
1 3anidm12.1 . . 3 ((𝜑𝜑𝜓) → 𝜒)
213expib 1123 . 2 (𝜑 → ((𝜑𝜓) → 𝜒))
32anabsi5 669 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1088
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 1090
This theorem is referenced by:  3anidm13  1421  syl2an3an  1423  dedth3v  4478  nncan  10996  divid  11408  sqdivid  13583  subsq  13667  o1lo1  14987  retancl  15590  tanneg  15596  gcd0id  15965  coprm  16155  ablonncan  28494  kbpj  29894  xdivid  30780  xrsmulgzz  30867  f1resrcmplf1dlem  32632  expgrowthi  41512  dvconstbi  41513  3ornot23  41690  3anidm12p2  41988  sinhpcosh  45925  reseccl  45938  recsccl  45939  recotcl  45940  onetansqsecsq  45946
  Copyright terms: Public domain W3C validator