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

Theorem imdistani 566
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 553 . 2 (𝜑 → (𝜓 → (𝜑𝜒)))
32imp 397 1 ((𝜑𝜓) → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386
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 199  df-an 387
This theorem is referenced by:  syldanl  597  cases2ALT  1077  difrab  4129  rabsnifsb  4474  foconst  6365  elfvmptrab  6553  dffo4  6623  dffo5  6624  isofrlem  6844  brfvopab  6959  onint  7255  el2mpt2cl  7513  tz7.48lem  7801  opthreg  8789  opthregOLD  8791  eltsk2g  9887  recgt1i  11249  sup2  11308  elnnnn0c  11664  elnnz1  11730  recnz  11779  eluz2b2  12043  iccsplit  12597  elfzp12  12712  1mod  12996  2swrd1eqwrdeqOLD  13743  pfxsuff1eqwrdeq  13777  cos01gt0  15292  oddnn02np1  15445  reumodprminv  15879  clatl  17468  isacs4lem  17520  isacs5lem  17521  isnzr2hash  19624  mplcoe5lem  19827  ioovolcl  23735  elply2  24350  cusgrsize  26751  rusgrpropedg  26881  wlkonprop  26954  wksonproplem  27006  pthdlem1  27067  clwwlknonex2lem2  27482  3oalem1  29075  elorrvc  31070  ballotlemfc0  31099  ballotlemfcc  31100  ballotlemodife  31104  ballotth  31144  opnrebl2  32853  bj-eldiag2  33620  topdifinffinlem  33739  finxpsuc  33779  wl-ax11-lem3  33907  matunitlindflem2  33949  matunitlindf  33950  poimirlem28  33980  poimirlem29  33981  mblfinlem1  33989  ovoliunnfl  33994  voliunnfl  33996  itg2addnclem2  34004  areacirclem5  34046  seqpo  34084  incsequz  34085  incsequz2  34086  ismtycnv  34142  prnc  34407  dihatexv2  37413  fperiodmullem  40314  climsuselem1  40633  climsuse  40634  0ellimcdiv  40675  fperdvper  40927  iblsplit  40975  stirlinglem11  41094  qndenserrnbllem  41304  sge0fodjrnlem  41423  2reu1  42010  upwlkbprop  42565  c0rnghm  42759  regt1loggt0  43176
  Copyright terms: Public domain W3C validator