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  3071  2reu1  3847  difrab  4270  rabsnifsb  4679  foconst  6761  elfvmptrab  6970  dffo4  7048  dffo5  7049  isofrlem  7286  brfvopab  7415  onint  7735  el2mpocl  8028  suppofssd  8145  tz7.48lem  8372  opthreg  9527  eltsk2g  10662  recgt1i  12039  sup2  12098  elnnnn0c  12446  elnnz1  12517  recnz  12567  eluz2b2  12834  iccsplit  13401  elfzp12  13519  1mod  13823  pfxsuff1eqwrdeq  14622  cos01gt0  16116  oddnn02np1  16275  reumodprminv  16732  clatl  18431  isacs4lem  18467  isacs5lem  18468  isnzr2hash  20452  c0rnghm  20468  isdomn4  20649  mplcoe5lem  21994  ioovolcl  25527  elply2  26157  cusgrsize  29528  rusgrpropedg  29658  wlkonprop  29730  wksonproplem  29776  pthdlem1  29839  3oalem1  31737  elorrvc  34621  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemodife  34655  ballotth  34695  nummin  35249  opnrebl2  36515  bj-eldiag2  37382  topdifinffinlem  37552  finxpsuc  37603  matunitlindflem2  37818  matunitlindf  37819  poimirlem28  37849  poimirlem29  37850  mblfinlem1  37858  ovoliunnfl  37863  voliunnfl  37865  itg2addnclem2  37873  areacirclem5  37913  seqpo  37948  incsequz  37949  incsequz2  37950  ismtycnv  38003  prnc  38268  dihatexv2  41599  unitscyglem4  42452  sn-sup2  42746  prjspval  42846  tfsconcatlem  43578  omssrncard  43781  reabsifneg  43873  reabsifnpos  43874  reabsifpos  43875  reabsifnneg  43876  relpfrlem  45194  fperiodmullem  45551  climsuselem1  45853  climsuse  45854  0ellimcdiv  45893  fperdvper  46163  iblsplit  46210  stirlinglem11  46328  qndenserrnbllem  46538  sge0fodjrnlem  46660  upwlkbprop  48384  regt1loggt0  48782