Theorem imdistani 570

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  syldanl  603  cases2ALT  1048  reximia  3082  2reu1  3892  difrab  4309  rabsnifsb  4727  foconst  6821  elfvmptrab  7027  dffo4  7105  dffo5  7106  isofrlem  7337  brfvopab  7466  onint  7778  el2mpocl  8072  suppofssd  8188  tz7.48lem  8441  opthreg  9613  eltsk2g  10746  recgt1i  12111  sup2  12170  elnnnn0c  12517  elnnz1  12588  recnz  12637  eluz2b2  12905  iccsplit  13462  elfzp12  13580  1mod  13868  pfxsuff1eqwrdeq  14649  cos01gt0  16134  oddnn02np1  16291  reumodprminv  16737  clatl  18461  isacs4lem  18497  isacs5lem  18498  isnzr2hash  20298  isdomn4  20918  mplcoe5lem  21594  ioovolcl  25087  elply2  25710  cusgrsize  28711  rusgrpropedg  28841  wlkonprop  28915  wksonproplem  28961  wksonproplemOLD  28962  pthdlem1  29023  3oalem1  30915  elorrvc  33462  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemodife  33496  ballotth  33536  nummin  34094  opnrebl2  35206  bj-eldiag2  36058  topdifinffinlem  36228  finxpsuc  36279  wl-ax11-lem3  36449  matunitlindflem2  36485  matunitlindf  36486  poimirlem28  36516  poimirlem29  36517  mblfinlem1  36525  ovoliunnfl  36530  voliunnfl  36532  itg2addnclem2  36540  areacirclem5  36580  seqpo  36615  incsequz  36616  incsequz2  36617  ismtycnv  36670  prnc  36935  dihatexv2  40210  sn-sup2  41342  prjspval  41345  tfsconcatlem  42086  omssrncard  42291  reabsifneg  42383  reabsifnpos  42384  reabsifpos  42385  reabsifnneg  42386  fperiodmullem  44013  climsuselem1  44323  climsuse  44324  0ellimcdiv  44365  fperdvper  44635  iblsplit  44682  stirlinglem11  44800  qndenserrnbllem  45010  sge0fodjrnlem  45132  upwlkbprop  46516  c0rnghm  46712  regt1loggt0  47222