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

Theorem imdistani 443
Description: Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)
Hypothesis
Ref Expression
imdistani.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
imdistani ((𝜑𝜓) → (𝜑𝜒))

Proof of Theorem imdistani
StepHypRef Expression
1 imdistani.1 . . 3 (𝜑 → (𝜓𝜒))
21anc2li 327 . 2 (𝜑 → (𝜓 → (𝜑𝜒)))
32imp 123 1 ((𝜑𝜓) → (𝜑𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  xoranor  1372  nfan1  1557  sbcof2  1803  difin  3364  difrab  3401  opthreg  4540  wessep  4562  fvelimab  5552  elfvmptrab  5591  dffo4  5644  dffo5  5645  ltaddpr  7559  recgt1i  8814  elnnnn0c  9180  elnnz1  9235  recnz  9305  eluz2b2  9562  elfzp12  10055  cos01gt0  11725  oddnn02np1  11839  reumodprminv  12207  sgrpidmndm  12656  bj-charfundc  13843
  Copyright terms: Public domain W3C validator