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

Theorem imdistani 442
Description: Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)
Hypothesis
Ref Expression
imdistani.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
imdistani  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ch ) )

Proof of Theorem imdistani
StepHypRef Expression
1 imdistani.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21anc2li 327 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ch ) ) )
32imp 123 1  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ch ) )
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  1356  nfan1  1544  sbcof2  1783  difin  3314  difrab  3351  opthreg  4475  wessep  4496  fvelimab  5481  elfvmptrab  5520  dffo4  5572  dffo5  5573  ltaddpr  7425  recgt1i  8676  elnnnn0c  9042  elnnz1  9097  recnz  9164  eluz2b2  9420  elfzp12  9906  cos01gt0  11496  oddnn02np1  11604
  Copyright terms: Public domain W3C validator