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

Theorem imdistani 721
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 577 . 2 (𝜑 → (𝜓 → (𝜑𝜒)))
32imp 443 1 ((𝜑𝜓) → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  syldanl  730  cases2  1004  nfan1OLD  2217  difrab  3854  rabsnifsb  4195  foconst  6019  elfvmptrab  6194  dffo4  6263  dffo5  6264  isofrlem  6463  brfvopab  6571  onint  6859  el2mpt2cl  7110  tz7.48lem  7395  opthreg  8370  eltsk2g  9424  recgt1i  10764  sup2  10823  elnnnn0c  11180  elnnz1  11231  recnz  11279  eluz2b2  11588  iccsplit  12127  elfzp12  12238  1mod  12514  2swrd1eqwrdeq  13247  cos01gt0  14701  oddnn02np1  14851  reumodprminv  15288  clatl  16880  isacs4lem  16932  isacs5lem  16933  isnzr2hash  19026  mplcoe5lem  19229  ioovolcl  23056  elply2  23668  wlkonprop  25824  trlonprop  25833  pthonprop  25868  spthonprp  25876  3oalem1  27706  elorrvc  29653  ballotlemfc0  29682  ballotlemfcc  29683  ballotlemodife  29687  ballotth  29727  opnrebl2  31287  bj-eldiag2  32067  topdifinffinlem  32169  finxpsuc  32209  wl-ax11-lem3  32341  matunitlindflem2  32374  matunitlindf  32375  poimirlem28  32405  poimirlem29  32406  mblfinlem1  32414  ovoliunnfl  32419  voliunnfl  32421  itg2addnclem2  32430  areacirclem5  32472  seqpo  32511  incsequz  32512  incsequz2  32513  ismtycnv  32569  prnc  32834  dihatexv2  35444  fperiodmullem  38256  climsuselem1  38473  climsuse  38474  0ellimcdiv  38515  fperdvper  38607  iblsplit  38657  stirlinglem11  38776  qndenserrnbllem  38989  sge0fodjrnlem  39108  2reu1  39634  pfxsuff1eqwrdeq  40070  cusgrsize  40667  rusgrpropedg  40781  wlkbProp  40814  wlkOnprop  40863  1wlksonproplem  40909  pthdlem1  40969  c0rnghm  41700  regt1loggt0  42125
  Copyright terms: Public domain W3C validator