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  3064  2reu1  3860  difrab  4281  rabsnifsb  4686  foconst  6787  elfvmptrab  6997  dffo4  7075  dffo5  7076  isofrlem  7315  brfvopab  7446  onint  7766  el2mpocl  8065  suppofssd  8182  tz7.48lem  8409  opthreg  9571  eltsk2g  10704  recgt1i  12080  sup2  12139  elnnnn0c  12487  elnnz1  12559  recnz  12609  eluz2b2  12880  iccsplit  13446  elfzp12  13564  1mod  13865  pfxsuff1eqwrdeq  14664  cos01gt0  16159  oddnn02np1  16318  reumodprminv  16775  clatl  18467  isacs4lem  18503  isacs5lem  18504  isnzr2hash  20428  c0rnghm  20444  isdomn4  20625  mplcoe5lem  21946  ioovolcl  25471  elply2  26101  cusgrsize  29382  rusgrpropedg  29512  wlkonprop  29586  wksonproplem  29632  wksonproplemOLD  29633  pthdlem1  29696  3oalem1  31591  elorrvc  34455  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemodife  34489  ballotth  34529  nummin  35081  opnrebl2  36309  bj-eldiag2  37165  topdifinffinlem  37335  finxpsuc  37386  wl-ax11-lem3  37575  matunitlindflem2  37611  matunitlindf  37612  poimirlem28  37642  poimirlem29  37643  mblfinlem1  37651  ovoliunnfl  37656  voliunnfl  37658  itg2addnclem2  37666  areacirclem5  37706  seqpo  37741  incsequz  37742  incsequz2  37743  ismtycnv  37796  prnc  38061  dihatexv2  41333  unitscyglem4  42186  sn-sup2  42479  prjspval  42591  tfsconcatlem  43325  omssrncard  43529  reabsifneg  43621  reabsifnpos  43622  reabsifpos  43623  reabsifnneg  43624  relpfrlem  44943  fperiodmullem  45301  climsuselem1  45605  climsuse  45606  0ellimcdiv  45647  fperdvper  45917  iblsplit  45964  stirlinglem11  46082  qndenserrnbllem  46292  sge0fodjrnlem  46414  upwlkbprop  48126  regt1loggt0  48525