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

Theorem imdistani 569
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 556 . 2 (𝜑 → (𝜓 → (𝜑𝜒)))
32imp 407 1 ((𝜑𝜓) → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  syldanl  601  cases2ALT  1040  2reu1  3880  difrab  4276  rabsnifsb  4652  foconst  6597  elfvmptrab  6789  dffo4  6862  dffo5  6863  isofrlem  7082  brfvopab  7200  onint  7498  el2mpocl  7772  suppofssd  7858  tz7.48lem  8068  opthreg  9070  eltsk2g  10162  recgt1i  11526  sup2  11586  elnnnn0c  11931  elnnz1  11997  recnz  12046  eluz2b2  12310  iccsplit  12861  elfzp12  12976  1mod  13261  pfxsuff1eqwrdeq  14051  cos01gt0  15534  oddnn02np1  15687  reumodprminv  16131  clatl  17716  isacs4lem  17768  isacs5lem  17769  isnzr2hash  19967  mplcoe5lem  20178  ioovolcl  24100  elply2  24715  cusgrsize  27164  rusgrpropedg  27294  wlkonprop  27368  wksonproplem  27414  pthdlem1  27475  3oalem1  29367  elorrvc  31621  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemodife  31655  ballotth  31695  opnrebl2  33567  bj-eldiag2  34362  topdifinffinlem  34511  finxpsuc  34562  wl-ax11-lem3  34701  matunitlindflem2  34771  matunitlindf  34772  poimirlem28  34802  poimirlem29  34803  mblfinlem1  34811  ovoliunnfl  34816  voliunnfl  34818  itg2addnclem2  34826  areacirclem5  34868  seqpo  34905  incsequz  34906  incsequz2  34907  ismtycnv  34963  prnc  35228  dihatexv2  38357  prjspval  39133  fperiodmullem  41450  climsuselem1  41768  climsuse  41769  0ellimcdiv  41810  fperdvper  42083  iblsplit  42131  stirlinglem11  42250  qndenserrnbllem  42460  sge0fodjrnlem  42579  upwlkbprop  43860  c0rnghm  44082  regt1loggt0  44494
  Copyright terms: Public domain W3C validator