Theorem imdistani 568

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 555	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))
3	2	imp 406	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  syldanl  602  cases2ALT  1048  reximia  3065  2reu1  3863  difrab  4284  rabsnifsb  4689  foconst  6790  elfvmptrab  7000  dffo4  7078  dffo5  7079  isofrlem  7318  brfvopab  7449  onint  7769  el2mpocl  8068  suppofssd  8185  tz7.48lem  8412  opthreg  9578  eltsk2g  10711  recgt1i  12087  sup2  12146  elnnnn0c  12494  elnnz1  12566  recnz  12616  eluz2b2  12887  iccsplit  13453  elfzp12  13571  1mod  13872  pfxsuff1eqwrdeq  14671  cos01gt0  16166  oddnn02np1  16325  reumodprminv  16782  clatl  18474  isacs4lem  18510  isacs5lem  18511  isnzr2hash  20435  c0rnghm  20451  isdomn4  20632  mplcoe5lem  21953  ioovolcl  25478  elply2  26108  cusgrsize  29389  rusgrpropedg  29519  wlkonprop  29593  wksonproplem  29639  wksonproplemOLD  29640  pthdlem1  29703  3oalem1  31598  elorrvc  34462  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemodife  34496  ballotth  34536  nummin  35088  opnrebl2  36316  bj-eldiag2  37172  topdifinffinlem  37342  finxpsuc  37393  wl-ax11-lem3  37582  matunitlindflem2  37618  matunitlindf  37619  poimirlem28  37649  poimirlem29  37650  mblfinlem1  37658  ovoliunnfl  37663  voliunnfl  37665  itg2addnclem2  37673  areacirclem5  37713  seqpo  37748  incsequz  37749  incsequz2  37750  ismtycnv  37803  prnc  38068  dihatexv2  41340  unitscyglem4  42193  sn-sup2  42486  prjspval  42598  tfsconcatlem  43332  omssrncard  43536  reabsifneg  43628  reabsifnpos  43629  reabsifpos  43630  reabsifnneg  43631  relpfrlem  44950  fperiodmullem  45308  climsuselem1  45612  climsuse  45613  0ellimcdiv  45654  fperdvper  45924  iblsplit  45971  stirlinglem11  46089  qndenserrnbllem  46299  sge0fodjrnlem  46421  upwlkbprop  48130  regt1loggt0  48529