Theorem imdistani 690

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

Step	Hyp	Ref	Expression
1		imdistani.1	. . 3
2	1	anc2li 557	. 2
3	2	imp 429	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  cases2  971  nfan1  1927  2eu1OLD  2377  difrab  3771  rabsnifsb  4098  foconst  5811  elfvmptrab  5977  dffo4  6047  dffo5  6048  isofrlem  6236  onint  6630  tz7.48lem  7125  opthreg  8056  axpowndlem3OLD  8997  eltsk2g  9150  recgt1i  10467  sup2  10524  elnnnn0c  10866  elnnz1  10915  recnz  10963  eluz2b2  11183  iccsplit  11682  elfzp12  11786  1mod  12028  2swrd1eqwrdeq  12679  cos01gt0  13926  reumodprminv  14329  clatl  15746  isacs4lem  15798  isacs5lem  15799  isnzr2hash  17912  mplcoe5lem  18130  ioovolcl  21979  elply2  22593  wlkonprop  24535  trlonprop  24544  pthonprop  24579  spthonprp  24587  3oalem1  26580  elorrvc  28402  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemodife  28436  ballotth  28476  wl-ax11-lem3  30027  mblfinlem1  30051  ovoliunnfl  30056  voliunnfl  30058  itg2addnclem2  30067  areacirclem5  30111  opnrebl2  30139  syldanl  30202  seqpo  30240  incsequz  30241  incsequz2  30242  ismtycnv  30298  prnc  30464  fperiodmullem  31503  climsuselem1  31613  climsuse  31614  0ellimcdiv  31655  fperdvper  31715  iblsplit  31765  stirlinglem11  31866  2reu1  32191  c0rnghm  32719  bj-eldiag2  34607  dihatexv2  37066

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 185  df-an 371