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

Theorem imdistani 726
 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 579 . 2 (𝜑 → (𝜓 → (𝜑𝜒)))
32imp 444 1 ((𝜑𝜓) → (𝜑𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 197  df-an 385 This theorem is referenced by:  syldanl  735  cases2ALT  1017  nfan1OLD  2272  difrab  3934  rabsnifsb  4289  foconst  6164  elfvmptrab  6345  dffo4  6415  dffo5  6416  isofrlem  6630  brfvopab  6742  onint  7037  el2mpt2cl  7296  tz7.48lem  7581  opthreg  8553  eltsk2g  9611  recgt1i  10958  sup2  11017  elnnnn0c  11376  elnnz1  11441  recnz  11490  eluz2b2  11799  iccsplit  12343  elfzp12  12457  1mod  12742  2swrd1eqwrdeq  13500  cos01gt0  14965  oddnn02np1  15119  reumodprminv  15556  clatl  17163  isacs4lem  17215  isacs5lem  17216  isnzr2hash  19312  mplcoe5lem  19515  ioovolcl  23384  elply2  23997  cusgrsize  26406  rusgrpropedg  26536  wlkonprop  26610  wksonproplem  26657  pthdlem1  26718  clwwlknonex2lem2  27083  3oalem1  28649  elorrvc  30653  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemodife  30687  ballotth  30727  opnrebl2  32441  bj-eldiag2  33222  topdifinffinlem  33325  finxpsuc  33365  wl-ax11-lem3  33494  matunitlindflem2  33536  matunitlindf  33537  poimirlem28  33567  poimirlem29  33568  mblfinlem1  33576  ovoliunnfl  33581  voliunnfl  33583  itg2addnclem2  33592  areacirclem5  33634  seqpo  33673  incsequz  33674  incsequz2  33675  ismtycnv  33731  prnc  33996  dihatexv2  36945  fperiodmullem  39831  climsuselem1  40157  climsuse  40158  0ellimcdiv  40199  fperdvper  40451  iblsplit  40500  stirlinglem11  40619  qndenserrnbllem  40832  sge0fodjrnlem  40951  2reu1  41507  pfxsuff1eqwrdeq  41732  upwlkbprop  42044  c0rnghm  42238  regt1loggt0  42655
 Copyright terms: Public domain W3C validator