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  3068  2reu1  3844  difrab  4267  rabsnifsb  4676  foconst  6757  elfvmptrab  6966  dffo4  7044  dffo5  7045  isofrlem  7282  brfvopab  7411  onint  7731  el2mpocl  8024  suppofssd  8141  tz7.48lem  8368  opthreg  9517  eltsk2g  10651  recgt1i  12028  sup2  12087  elnnnn0c  12435  elnnz1  12506  recnz  12556  eluz2b2  12823  iccsplit  13389  elfzp12  13507  1mod  13811  pfxsuff1eqwrdeq  14610  cos01gt0  16104  oddnn02np1  16263  reumodprminv  16720  clatl  18418  isacs4lem  18454  isacs5lem  18455  isnzr2hash  20438  c0rnghm  20454  isdomn4  20635  mplcoe5lem  21977  ioovolcl  25501  elply2  26131  cusgrsize  29437  rusgrpropedg  29567  wlkonprop  29639  wksonproplem  29685  pthdlem1  29748  3oalem1  31646  elorrvc  34500  ballotlemfc0  34529  ballotlemfcc  34530  ballotlemodife  34534  ballotth  34574  nummin  35127  opnrebl2  36388  bj-eldiag2  37244  topdifinffinlem  37414  finxpsuc  37465  matunitlindflem2  37680  matunitlindf  37681  poimirlem28  37711  poimirlem29  37712  mblfinlem1  37720  ovoliunnfl  37725  voliunnfl  37727  itg2addnclem2  37735  areacirclem5  37775  seqpo  37810  incsequz  37811  incsequz2  37812  ismtycnv  37865  prnc  38130  dihatexv2  41461  unitscyglem4  42314  sn-sup2  42612  prjspval  42724  tfsconcatlem  43456  omssrncard  43660  reabsifneg  43752  reabsifnpos  43753  reabsifpos  43754  reabsifnneg  43755  relpfrlem  45073  fperiodmullem  45431  climsuselem1  45734  climsuse  45735  0ellimcdiv  45774  fperdvper  46044  iblsplit  46091  stirlinglem11  46209  qndenserrnbllem  46419  sge0fodjrnlem  46541  upwlkbprop  48265  regt1loggt0  48664