Theorem imdistani 572

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  syldanl  604  cases2ALT  1044  2reu1  3826  difrab  4229  rabsnifsb  4618  foconst  6578  elfvmptrab  6773  dffo4  6846  dffo5  6847  isofrlem  7072  brfvopab  7190  onint  7490  el2mpocl  7764  suppofssd  7850  tz7.48lem  8060  opthreg  9065  eltsk2g  10162  recgt1i  11526  sup2  11584  elnnnn0c  11930  elnnz1  11996  recnz  12045  eluz2b2  12309  iccsplit  12863  elfzp12  12981  1mod  13266  pfxsuff1eqwrdeq  14052  cos01gt0  15536  oddnn02np1  15689  reumodprminv  16131  clatl  17718  isacs4lem  17770  isacs5lem  17771  isnzr2hash  20030  mplcoe5lem  20707  ioovolcl  24174  elply2  24793  cusgrsize  27244  rusgrpropedg  27374  wlkonprop  27448  wksonproplem  27494  pthdlem1  27555  3oalem1  29445  elorrvc  31831  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemodife  31865  ballotth  31905  nummin  32474  opnrebl2  33782  bj-eldiag2  34592  topdifinffinlem  34764  finxpsuc  34815  wl-ax11-lem3  34984  matunitlindflem2  35054  matunitlindf  35055  poimirlem28  35085  poimirlem29  35086  mblfinlem1  35094  ovoliunnfl  35099  voliunnfl  35101  itg2addnclem2  35109  areacirclem5  35149  seqpo  35185  incsequz  35186  incsequz2  35187  ismtycnv  35240  prnc  35505  dihatexv2  38635  sn-sup2  39594  prjspval  39597  reabsifneg  40332  reabsifnpos  40333  reabsifpos  40334  reabsifnneg  40335  fperiodmullem  41935  climsuselem1  42249  climsuse  42250  0ellimcdiv  42291  fperdvper  42561  iblsplit  42608  stirlinglem11  42726  qndenserrnbllem  42936  sge0fodjrnlem  43055  upwlkbprop  44366  c0rnghm  44537  regt1loggt0  44950