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

Theorem 3anidm12 1529
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 1116 . 2 (𝜑 → ((𝜑𝜓) → 𝜒))
32anabsi5 648 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  3anidm13  1530  syl2an3an  1532  dedth3v  4283  nncan  10512  divid  10916  sqdivid  13136  subsq  13179  o1lo1  14476  retancl  15078  tanneg  15084  gcd0id  15448  coprm  15630  ablonncan  27751  kbpj  29155  xdivid  29976  xrsmulgzz  30018  expgrowthi  39058  dvconstbi  39059  3ornot23  39240  3anidm12p2  39559  sinhpcosh  43012  reseccl  43025  recsccl  43026  recotcl  43027  onetansqsecsq  43033
  Copyright terms: Public domain W3C validator