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

Theorem imdistani 672
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 541 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ch ) ) )
32imp 419 1  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  nfan1  1845  2eu1  2361  difrab  3615  onint  4775  foconst  5664  dffo4  5885  dffo5  5886  isofrlem  6060  tz7.48lem  6698  opthreg  7573  axpowndlem3  8474  eltsk2g  8626  recgt1i  9907  sup2  9964  elnnnn0c  10265  elnnz1  10307  recnz  10345  eluz2b2  10548  iccsplit  11029  elfzp12  11126  1mod  11273  cos01gt0  12792  clatl  14543  isacs4lem  14594  isacs5lem  14595  elply2  20115  wlkonprop  21532  trlonprop  21542  pthonprop  21577  spthonprp  21585  3oalem1  23164  elorrvc  24721  ballotlemfc0  24750  ballotlemfcc  24751  ballotlemodife  24755  ballotth  24795  mblfinlem1  26243  ovoliunnfl  26248  voliunnfl  26250  itg2addnclem2  26257  areacirclem5  26296  opnrebl2  26324  syldanl  26413  seqpo  26451  incsequz  26452  incsequz2  26453  ismtycnv  26511  prnc  26677  climsuselem1  27709  climsuse  27710  ioovolcl  27718  stirlinglem11  27809  2reu1  27940  reumodprminv  28227  ax7w9AUX7  29660  ax7w10AUX7  29662  dihatexv2  32137
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator