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

Theorem imdistani 725
 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 445 1 ((𝜑𝜓) → (𝜑𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384 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 386 This theorem is referenced by:  syldanl  734  cases2  992  nfan1OLD  2234  difrab  3893  rabsnifsb  4248  foconst  6113  elfvmptrab  6292  dffo4  6361  dffo5  6362  isofrlem  6575  brfvopab  6685  onint  6980  el2mpt2cl  7236  tz7.48lem  7521  opthreg  8500  eltsk2g  9558  recgt1i  10905  sup2  10964  elnnnn0c  11323  elnnz1  11388  recnz  11437  eluz2b2  11746  iccsplit  12290  elfzp12  12403  1mod  12685  2swrd1eqwrdeq  13436  cos01gt0  14902  oddnn02np1  15053  reumodprminv  15490  clatl  17097  isacs4lem  17149  isacs5lem  17150  isnzr2hash  19245  mplcoe5lem  19448  ioovolcl  23319  elply2  23933  cusgrsize  26331  rusgrpropedg  26461  wlkonprop  26535  wksonproplem  26582  pthdlem1  26643  3oalem1  28491  elorrvc  30499  ballotlemfc0  30528  ballotlemfcc  30529  ballotlemodife  30533  ballotth  30573  opnrebl2  32291  bj-eldiag2  33063  topdifinffinlem  33166  finxpsuc  33206  wl-ax11-lem3  33335  matunitlindflem2  33377  matunitlindf  33378  poimirlem28  33408  poimirlem29  33409  mblfinlem1  33417  ovoliunnfl  33422  voliunnfl  33424  itg2addnclem2  33433  areacirclem5  33475  seqpo  33514  incsequz  33515  incsequz2  33516  ismtycnv  33572  prnc  33837  dihatexv2  36447  fperiodmullem  39330  climsuselem1  39639  climsuse  39640  0ellimcdiv  39681  fperdvper  39896  iblsplit  39945  stirlinglem11  40064  qndenserrnbllem  40277  sge0fodjrnlem  40396  2reu1  40949  pfxsuff1eqwrdeq  41172  upwlkbprop  41484  c0rnghm  41678  regt1loggt0  42095
 Copyright terms: Public domain W3C validator