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

Theorem imdistani 441
 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  1355  nfan1  1543  sbcof2  1782  difin  3313  difrab  3350  opthreg  4471  wessep  4492  fvelimab  5477  elfvmptrab  5516  dffo4  5568  dffo5  5569  ltaddpr  7405  recgt1i  8656  elnnnn0c  9022  elnnz1  9077  recnz  9144  eluz2b2  9397  elfzp12  9879  cos01gt0  11469  oddnn02np1  11577
 Copyright terms: Public domain W3C validator