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

Theorem imdistani 427
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 316 . 2 (𝜑 → (𝜓 → (𝜑𝜒)))
32imp 119 1 ((𝜑𝜓) → (𝜑𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  xoranor  1284  nfan1  1472  sbcof2  1707  difin  3202  difrab  3239  opthreg  4308  wessep  4330  fvelimab  5257  dffo4  5343  dffo5  5344  ltaddpr  6753  recgt1i  7939  elnnnn0c  8284  elnnz1  8325  recnz  8391  eluz2b2  8637  elfzp12  9063  oddnn02np1  10192
  Copyright terms: Public domain W3C validator