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  3878  difrab  4274  rabsnifsb  4650  foconst  6596  elfvmptrab  6788  dffo4  6861  dffo5  6862  isofrlem  7082  brfvopab  7200  onint  7499  el2mpocl  7770  suppofssd  7856  tz7.48lem  8066  opthreg  9069  eltsk2g  10161  recgt1i  11525  sup2  11585  elnnnn0c  11930  elnnz1  11996  recnz  12045  eluz2b2  12309  iccsplit  12859  elfzp12  12974  1mod  13259  pfxsuff1eqwrdeq  14049  cos01gt0  15532  oddnn02np1  15685  reumodprminv  16129  clatl  17714  isacs4lem  17766  isacs5lem  17767  isnzr2hash  19965  mplcoe5lem  20176  ioovolcl  24098  elply2  24713  cusgrsize  27163  rusgrpropedg  27293  wlkonprop  27367  wksonproplem  27413  pthdlem1  27474  3oalem1  29366  elorrvc  31620  ballotlemfc0  31649  ballotlemfcc  31650  ballotlemodife  31654  ballotth  31694  opnrebl2  33566  bj-eldiag2  34361  topdifinffinlem  34510  finxpsuc  34561  wl-ax11-lem3  34700  matunitlindflem2  34770  matunitlindf  34771  poimirlem28  34801  poimirlem29  34802  mblfinlem1  34810  ovoliunnfl  34815  voliunnfl  34817  itg2addnclem2  34825  areacirclem5  34867  seqpo  34903  incsequz  34904  incsequz2  34905  ismtycnv  34961  prnc  35226  dihatexv2  38355  prjspval  39131  fperiodmullem  41446  climsuselem1  41764  climsuse  41765  0ellimcdiv  41806  fperdvper  42079  iblsplit  42127  stirlinglem11  42246  qndenserrnbllem  42456  sge0fodjrnlem  42575  upwlkbprop  43890  c0rnghm  44112  regt1loggt0  44524
  Copyright terms: Public domain W3C validator