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

Theorem imdistani 570
Description: Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)
Hypothesis
Ref Expression
imdistani.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
imdistani ((𝜑𝜓) → (𝜑𝜒))

Proof of Theorem imdistani
StepHypRef Expression
1 imdistani.1 . . 3 (𝜑 → (𝜓𝜒))
21anc2li 557 . 2 (𝜑 → (𝜓 → (𝜑𝜒)))
32imp 408 1 ((𝜑𝜓) → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  syldanl  603  cases2ALT  1048  reximia  3083  2reu1  3852  difrab  4267  rabsnifsb  4682  foconst  6767  elfvmptrab  6972  dffo4  7048  dffo5  7049  isofrlem  7280  brfvopab  7407  onint  7716  el2mpocl  8007  suppofssd  8102  tz7.48lem  8355  opthreg  9488  eltsk2g  10621  recgt1i  11986  sup2  12045  elnnnn0c  12392  elnnz1  12460  recnz  12509  eluz2b2  12775  iccsplit  13331  elfzp12  13449  1mod  13737  pfxsuff1eqwrdeq  14519  cos01gt0  16008  oddnn02np1  16165  reumodprminv  16611  clatl  18332  isacs4lem  18368  isacs5lem  18369  isnzr2hash  20658  mplcoe5lem  21363  ioovolcl  24857  elply2  25480  cusgrsize  28201  rusgrpropedg  28331  wlkonprop  28405  wksonproplem  28451  wksonproplemOLD  28452  pthdlem1  28513  3oalem1  30403  elorrvc  32837  ballotlemfc0  32866  ballotlemfcc  32867  ballotlemodife  32871  ballotth  32911  nummin  33469  opnrebl2  34689  bj-eldiag2  35544  topdifinffinlem  35714  finxpsuc  35765  wl-ax11-lem3  35935  matunitlindflem2  35971  matunitlindf  35972  poimirlem28  36002  poimirlem29  36003  mblfinlem1  36011  ovoliunnfl  36016  voliunnfl  36018  itg2addnclem2  36026  areacirclem5  36066  seqpo  36102  incsequz  36103  incsequz2  36104  ismtycnv  36157  prnc  36422  dihatexv2  39698  isdomn4  40520  sn-sup2  40804  prjspval  40807  omssrncard  41575  reabsifneg  41667  reabsifnpos  41668  reabsifpos  41669  reabsifnneg  41670  fperiodmullem  43295  climsuselem1  43602  climsuse  43603  0ellimcdiv  43644  fperdvper  43914  iblsplit  43961  stirlinglem11  44079  qndenserrnbllem  44289  sge0fodjrnlem  44411  upwlkbprop  45790  c0rnghm  45961  regt1loggt0  46372
  Copyright terms: Public domain W3C validator