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  1042  2reu1  3885  difrab  4281  rabsnifsb  4657  foconst  6600  elfvmptrab  6792  dffo4  6865  dffo5  6866  isofrlem  7085  brfvopab  7203  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  19956  mplcoe5lem  20166  ioovolcl  24086  elply2  24701  cusgrsize  27150  rusgrpropedg  27280  wlkonprop  27354  wksonproplem  27400  pthdlem1  27461  3oalem1  29353  elorrvc  31607  ballotlemfc0  31636  ballotlemfcc  31637  ballotlemodife  31641  ballotth  31681  opnrebl2  33553  bj-eldiag2  34348  topdifinffinlem  34497  finxpsuc  34548  wl-ax11-lem3  34686  matunitlindflem2  34756  matunitlindf  34757  poimirlem28  34787  poimirlem29  34788  mblfinlem1  34796  ovoliunnfl  34801  voliunnfl  34803  itg2addnclem2  34811  areacirclem5  34853  seqpo  34890  incsequz  34891  incsequz2  34892  ismtycnv  34948  prnc  35213  dihatexv2  38342  prjspval  39118  fperiodmullem  41435  climsuselem1  41753  climsuse  41754  0ellimcdiv  41795  fperdvper  42068  iblsplit  42116  stirlinglem11  42235  qndenserrnbllem  42445  sge0fodjrnlem  42564  upwlkbprop  43845  c0rnghm  44016  regt1loggt0  44428
 Copyright terms: Public domain W3C validator