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

Theorem imdistani 701
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 564 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ch ) ) )
32imp 435 1  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  syldanl  710  cases2  989  nfan1  2021  difrab  3729  rabsnifsb  4053  foconst  5827  elfvmptrab  5994  dffo4  6061  dffo5  6062  isofrlem  6256  brfvopab  6363  onint  6649  tz7.48lem  7184  opthreg  8149  eltsk2g  9202  recgt1i  10531  sup2  10593  elnnnn0c  10944  elnnz1  10992  recnz  11040  eluz2b2  11260  iccsplit  11794  elfzp12  11902  1mod  12161  2swrd1eqwrdeq  12847  cos01gt0  14294  reumodprminv  14804  clatl  16411  isacs4lem  16463  isacs5lem  16464  isnzr2hash  18537  mplcoe5lem  18740  ioovolcl  22571  elply2  23199  wlkonprop  25312  trlonprop  25321  pthonprop  25356  spthonprp  25364  3oalem1  27364  elorrvc  29345  ballotlemfc0  29374  ballotlemfcc  29375  ballotlemodife  29379  ballotth  29419  ballotthOLD  29457  opnrebl2  31026  bj-eldiag2  31692  topdifinffinlem  31795  finxpsuc  31835  wl-ax11-lem3  31962  poimirlem28  32013  poimirlem29  32014  mblfinlem1  32022  ovoliunnfl  32027  voliunnfl  32029  itg2addnclem2  32039  areacirclem5  32081  seqpo  32121  incsequz  32122  incsequz2  32123  ismtycnv  32179  prnc  32345  dihatexv2  34952  fperiodmullem  37559  climsuselem1  37724  climsuse  37725  0ellimcdiv  37768  fperdvper  37828  iblsplit  37881  stirlinglem11  37984  qndenserrnbllem  38201  sge0fodjrnlem  38296  2reu1  38645  pfxsuff1eqwrdeq  38988  cusgrsize  39565  rusgrpropedg  39650  wlkbProp  39680  wlkOnprop  39709  1wlksonproplem  39740  pthdlem1  39792  c0rnghm  40186  regt1loggt0  40620
  Copyright terms: Public domain W3C validator