Theorem imdistani 569

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  syldanl  602  cases2ALT  1047  reximia  3081  2reu1  3891  difrab  4308  rabsnifsb  4726  foconst  6820  elfvmptrab  7026  dffo4  7104  dffo5  7105  isofrlem  7339  brfvopab  7468  onint  7780  el2mpocl  8074  suppofssd  8190  tz7.48lem  8443  opthreg  9615  eltsk2g  10748  recgt1i  12113  sup2  12172  elnnnn0c  12519  elnnz1  12590  recnz  12639  eluz2b2  12907  iccsplit  13464  elfzp12  13582  1mod  13870  pfxsuff1eqwrdeq  14651  cos01gt0  16136  oddnn02np1  16293  reumodprminv  16739  clatl  18463  isacs4lem  18499  isacs5lem  18500  isnzr2hash  20302  isdomn4  20924  mplcoe5lem  21600  ioovolcl  25094  elply2  25717  cusgrsize  28749  rusgrpropedg  28879  wlkonprop  28953  wksonproplem  28999  wksonproplemOLD  29000  pthdlem1  29061  3oalem1  30953  elorrvc  33531  ballotlemfc0  33560  ballotlemfcc  33561  ballotlemodife  33565  ballotth  33605  nummin  34163  opnrebl2  35292  bj-eldiag2  36144  topdifinffinlem  36314  finxpsuc  36365  wl-ax11-lem3  36535  matunitlindflem2  36571  matunitlindf  36572  poimirlem28  36602  poimirlem29  36603  mblfinlem1  36611  ovoliunnfl  36616  voliunnfl  36618  itg2addnclem2  36626  areacirclem5  36666  seqpo  36701  incsequz  36702  incsequz2  36703  ismtycnv  36756  prnc  37021  dihatexv2  40296  sn-sup2  41424  prjspval  41427  tfsconcatlem  42168  omssrncard  42373  reabsifneg  42465  reabsifnpos  42466  reabsifpos  42467  reabsifnneg  42468  fperiodmullem  44092  climsuselem1  44402  climsuse  44403  0ellimcdiv  44444  fperdvper  44714  iblsplit  44761  stirlinglem11  44879  qndenserrnbllem  45089  sge0fodjrnlem  45211  upwlkbprop  46595  c0rnghm  46791  regt1loggt0  47300