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

Theorem imdistani 671
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 540 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ch ) ) )
32imp 418 1  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  nfan1  1834  2eu1  2236  difrab  3455  onint  4602  foconst  5478  dffo4  5692  dffo5  5693  isofrlem  5853  tz7.48lem  6469  opthreg  7335  axpowndlem3  8237  eltsk2g  8389  recgt1i  9669  sup2  9726  elnnnn0c  10025  elnnz1  10065  recnz  10103  eluz2b2  10306  iccsplit  10784  elfzp12  10877  1mod  11012  cos01gt0  12487  clatl  14236  isacs4lem  14287  isacs5lem  14288  elply2  19594  3oalem1  22257  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemodife  23072  ballotth  23112  measvunilem  23555  probun  23637  elorrvc  23679  ovoliunnfl  25001  itg2addnclem2  25004  itg2addnc  25005  areacirclem6  25033  tolat  25389  ablocomgrp  25445  setiscat  26082  opnrebl2  26339  syldanl  26437  seqpo  26560  incsequz  26561  incsequz2  26562  ismtycnv  26629  prnc  26795  climsuselem1  27836  climsuse  27837  ioovolcl  27845  stirlinglem11  27936  2reu1  28067  trlonprop  28341  ax7w9AUX7  29630  dihatexv2  32151
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 177  df-an 360
  Copyright terms: Public domain W3C validator