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

Theorem imdistani 690
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 557 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ch ) ) )
32imp 429 1  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  cases2  963  nfan1  1860  2eu1OLD  2365  difrab  3636  rabsnifsb  3955  foconst  5643  dffo4  5871  dffo5  5872  isofrlem  6043  onint  6418  tz7.48lem  6908  opthreg  7836  axpowndlem3OLD  8777  eltsk2g  8930  recgt1i  10241  sup2  10298  elnnnn0c  10637  elnnz1  10684  recnz  10729  eluz2b2  10939  iccsplit  11430  elfzp12  11551  1mod  11752  2swrd1eqwrdeq  12360  cos01gt0  13487  reumodprminv  13884  clatl  15298  isacs4lem  15350  isacs5lem  15351  mplcoe5lem  17559  ioovolcl  21062  elply2  21676  wlkonprop  23443  trlonprop  23453  pthonprop  23488  spthonprp  23496  3oalem1  25077  elorrvc  26858  ballotlemfc0  26887  ballotlemfcc  26888  ballotlemodife  26892  ballotth  26932  wl-ax11-lem3  28415  mblfinlem1  28440  ovoliunnfl  28445  voliunnfl  28447  itg2addnclem2  28456  areacirclem5  28500  opnrebl2  28528  syldanl  28617  seqpo  28655  incsequz  28656  incsequz2  28657  ismtycnv  28713  prnc  28879  climsuselem1  29792  climsuse  29793  stirlinglem11  29891  2reu1  30022  elfvmptrab  30167  isnzr2hash  30786  dihatexv2  34996
  Copyright terms: Public domain W3C validator