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  1049  reximia  3081  2reu1  3897  difrab  4318  rabsnifsb  4722  foconst  6835  elfvmptrab  7045  dffo4  7123  dffo5  7124  isofrlem  7360  brfvopab  7490  onint  7810  el2mpocl  8111  suppofssd  8228  tz7.48lem  8481  opthreg  9658  eltsk2g  10791  recgt1i  12165  sup2  12224  elnnnn0c  12571  elnnz1  12643  recnz  12693  eluz2b2  12963  iccsplit  13525  elfzp12  13643  1mod  13943  pfxsuff1eqwrdeq  14737  cos01gt0  16227  oddnn02np1  16385  reumodprminv  16842  clatl  18553  isacs4lem  18589  isacs5lem  18590  isnzr2hash  20519  c0rnghm  20535  isdomn4  20716  mplcoe5lem  22057  ioovolcl  25605  elply2  26235  cusgrsize  29472  rusgrpropedg  29602  wlkonprop  29676  wksonproplem  29722  wksonproplemOLD  29723  pthdlem1  29786  3oalem1  31681  elorrvc  34466  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemodife  34500  ballotth  34540  nummin  35105  opnrebl2  36322  bj-eldiag2  37178  topdifinffinlem  37348  finxpsuc  37399  wl-ax11-lem3  37588  matunitlindflem2  37624  matunitlindf  37625  poimirlem28  37655  poimirlem29  37656  mblfinlem1  37664  ovoliunnfl  37669  voliunnfl  37671  itg2addnclem2  37679  areacirclem5  37719  seqpo  37754  incsequz  37755  incsequz2  37756  ismtycnv  37809  prnc  38074  dihatexv2  41341  unitscyglem4  42199  sn-sup2  42501  prjspval  42613  tfsconcatlem  43349  omssrncard  43553  reabsifneg  43645  reabsifnpos  43646  reabsifpos  43647  reabsifnneg  43648  relpfrlem  44974  fperiodmullem  45315  climsuselem1  45622  climsuse  45623  0ellimcdiv  45664  fperdvper  45934  iblsplit  45981  stirlinglem11  46099  qndenserrnbllem  46309  sge0fodjrnlem  46431  upwlkbprop  48054  regt1loggt0  48457