MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imdistani Structured version   Unicode version

Theorem imdistani 694
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 559 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ch ) ) )
32imp 430 1  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372
This theorem is referenced by:  syldanl  703  cases2  980  nfan1  1983  2eu1OLD  2351  difrab  3747  rabsnifsb  4065  foconst  5817  elfvmptrab  5983  dffo4  6049  dffo5  6050  isofrlem  6242  onint  6632  tz7.48lem  7162  opthreg  8125  eltsk2g  9176  recgt1i  10503  sup2  10565  elnnnn0c  10915  elnnz1  10963  recnz  11011  eluz2b2  11231  iccsplit  11765  elfzp12  11873  1mod  12128  2swrd1eqwrdeq  12800  cos01gt0  14232  reumodprminv  14742  clatl  16349  isacs4lem  16401  isacs5lem  16402  isnzr2hash  18475  mplcoe5lem  18678  ioovolcl  22508  elply2  23136  wlkonprop  25248  trlonprop  25257  pthonprop  25292  spthonprp  25300  3oalem1  27300  elorrvc  29291  ballotlemfc0  29320  ballotlemfcc  29321  ballotlemodife  29325  ballotth  29365  ballotthOLD  29403  opnrebl2  30969  bj-eldiag2  31598  topdifinffinlem  31690  wl-ax11-lem3  31830  poimirlem28  31881  poimirlem29  31882  mblfinlem1  31890  ovoliunnfl  31895  voliunnfl  31897  itg2addnclem2  31907  areacirclem5  31949  seqpo  31989  incsequz  31990  incsequz2  31991  ismtycnv  32047  prnc  32213  dihatexv2  34825  fperiodmullem  37362  climsuselem1  37505  climsuse  37506  0ellimcdiv  37549  fperdvper  37609  iblsplit  37662  stirlinglem11  37765  sge0fodjrnlem  38045  2reu1  38319  pfxsuff1eqwrdeq  38659  c0rnghm  39184  regt1loggt0  39620
  Copyright terms: Public domain W3C validator