ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3anidm12 GIF version

Theorem 3anidm12 1295
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 1206 . 2 (𝜑 → ((𝜑𝜓) → 𝜒))
32anabsi5 579 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  3anidm13  1296  syl2an3an  1298  prarloclemarch2  7420  nq02m  7466  recexprlem1ssl  7634  recexprlem1ssu  7635  nncan  8188  dividap  8660  modqid0  10352  sqdividap  10587  subsq  10629  retanclap  11732  tannegap  11738  gcd0id  11982  coprm  12146
  Copyright terms: Public domain W3C validator