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

Theorem 3anidm12 1543
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 1153 . 2 (𝜑 → ((𝜑𝜓) → 𝜒))
32anabsi5 660 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  w3a 1108
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 386  df-3an 1110
This theorem is referenced by:  3anidm13  1544  syl2an3an  1546  dedth3v  4338  nncan  10602  divid  11006  sqdivid  13183  subsq  13226  o1lo1  14609  retancl  15208  tanneg  15214  gcd0id  15575  coprm  15756  ablonncan  27936  kbpj  29340  xdivid  30152  xrsmulgzz  30194  expgrowthi  39314  dvconstbi  39315  3ornot23  39495  3anidm12p2  39803  sinhpcosh  43283  reseccl  43296  recsccl  43297  recotcl  43298  onetansqsecsq  43304
  Copyright terms: Public domain W3C validator