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  20657  mplcoe5lem  21362  ioovolcl  24856  elply2  25479  cusgrsize  28188  rusgrpropedg  28318  wlkonprop  28392  wksonproplem  28438  wksonproplemOLD  28439  pthdlem1  28500  3oalem1  30390  elorrvc  32824  ballotlemfc0  32853  ballotlemfcc  32854  ballotlemodife  32858  ballotth  32898  nummin  33456  opnrebl2  34679  bj-eldiag2  35534  topdifinffinlem  35704  finxpsuc  35755  wl-ax11-lem3  35925  matunitlindflem2  35961  matunitlindf  35962  poimirlem28  35992  poimirlem29  35993  mblfinlem1  36001  ovoliunnfl  36006  voliunnfl  36008  itg2addnclem2  36016  areacirclem5  36056  seqpo  36092  incsequz  36093  incsequz2  36094  ismtycnv  36147  prnc  36412  dihatexv2  39688  isdomn4  40510  sn-sup2  40772  prjspval  40775  omssrncard  41543  reabsifneg  41635  reabsifnpos  41636  reabsifpos  41637  reabsifnneg  41638  fperiodmullem  43263  climsuselem1  43570  climsuse  43571  0ellimcdiv  43612  fperdvper  43882  iblsplit  43929  stirlinglem11  44047  qndenserrnbllem  44257  sge0fodjrnlem  44379  upwlkbprop  45758  c0rnghm  45929  regt1loggt0  46340
  Copyright terms: Public domain W3C validator