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  603  cases2ALT  1049  reximia  3073  2reu1  3836  difrab  4259  rabsnifsb  4667  foconst  6761  elfvmptrab  6971  dffo4  7049  dffo5  7050  isofrlem  7288  brfvopab  7417  onint  7737  el2mpocl  8029  suppofssd  8146  tz7.48lem  8373  opthreg  9530  eltsk2g  10665  recgt1i  12044  sup2  12103  elnnnn0c  12473  elnnz1  12544  recnz  12595  eluz2b2  12862  iccsplit  13429  elfzp12  13548  1mod  13853  pfxsuff1eqwrdeq  14652  cos01gt0  16149  oddnn02np1  16308  reumodprminv  16766  clatl  18465  isacs4lem  18501  isacs5lem  18502  isnzr2hash  20487  c0rnghm  20503  isdomn4  20684  mplcoe5lem  22027  ioovolcl  25547  elply2  26171  cusgrsize  29538  rusgrpropedg  29668  wlkonprop  29740  wksonproplem  29786  pthdlem1  29849  3oalem1  31748  elorrvc  34624  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemodife  34658  ballotth  34698  nummin  35252  opnrebl2  36519  bj-eldiag2  37507  topdifinffinlem  37677  finxpsuc  37728  matunitlindflem2  37952  matunitlindf  37953  poimirlem28  37983  poimirlem29  37984  mblfinlem1  37992  ovoliunnfl  37997  voliunnfl  37999  itg2addnclem2  38007  areacirclem5  38047  seqpo  38082  incsequz  38083  incsequz2  38084  ismtycnv  38137  prnc  38402  dihatexv2  41799  unitscyglem4  42651  sn-sup2  42950  prjspval  43050  tfsconcatlem  43782  omssrncard  43985  reabsifneg  44077  reabsifnpos  44078  reabsifpos  44079  reabsifnneg  44080  relpfrlem  45398  fperiodmullem  45754  climsuselem1  46055  climsuse  46056  0ellimcdiv  46095  fperdvper  46365  iblsplit  46412  stirlinglem11  46530  qndenserrnbllem  46740  sge0fodjrnlem  46862  upwlkbprop  48626  regt1loggt0  49024