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

Theorem imdistani 445
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 329 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ch ) ) )
32imp 124 1  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
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 is referenced by:  syldanl  449  xoranor  1377  nfan1  1564  sbcof2  1810  difin  3372  difrab  3409  opthreg  4552  wessep  4574  fvelimab  5568  elfvmptrab  5607  dffo4  5660  dffo5  5661  ltaddpr  7584  recgt1i  8841  elnnnn0c  9207  elnnz1  9262  recnz  9332  eluz2b2  9589  elfzp12  10082  cos01gt0  11751  oddnn02np1  11865  reumodprminv  12233  sgrpidmndm  12710  bj-charfundc  14213
  Copyright terms: Public domain W3C validator