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

Theorem 3anidm12 1546
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 1156 . 2 (𝜑 → ((𝜑𝜓) → 𝜒))
32anabsi5 659 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1111
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 199  df-an 387  df-3an 1113
This theorem is referenced by:  3anidm13  1547  syl2an3an  1549  dedth3v  4369  nncan  10638  divid  11046  sqdivid  13230  subsq  13273  o1lo1  14652  retancl  15251  tanneg  15257  gcd0id  15620  coprm  15801  ablonncan  27962  kbpj  29366  xdivid  30177  xrsmulgzz  30219  expgrowthi  39367  dvconstbi  39368  3ornot23  39548  3anidm12p2  39856  sinhpcosh  43389  reseccl  43402  recsccl  43403  recotcl  43404  onetansqsecsq  43410
  Copyright terms: Public domain W3C validator