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

Theorem 3anidm12 1380
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 1265 . 2 (𝜑 → ((𝜑𝜓) → 𝜒))
32anabsi5 857 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  3anidm13  1381  syl2an3an  1383  dedth3v  4121  nncan  10262  divid  10666  sqdivid  12877  subsq  12920  o1lo1  14210  retancl  14808  tanneg  14814  gcd0id  15175  coprm  15358  ablonncan  27281  kbpj  28685  xdivid  29445  xrsmulgzz  29487  expgrowthi  38049  dvconstbi  38050  3ornot23  38232  3anidm12p2  38551  sinhpcosh  41800  reseccl  41813  recsccl  41814  recotcl  41815  onetansqsecsq  41821
  Copyright terms: Public domain W3C validator