Theorem ancld 551

Description: Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)

Hypothesis

Ref	Expression
ancld.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
ancld	⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜒)))

Proof of Theorem ancld

Step	Hyp	Ref	Expression
1		idd 24	. 2 ⊢ (𝜑 → (𝜓 → 𝜓))
2		ancld.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	jcad 513	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:  dfmoeu  2536  mopick2  2639  2eu6  2658  cgsexg  3474  cgsex2g  3475  cgsex4g  3476  cgsex4gOLD  3477  ss2abdv  3997  reximdva0  4285  difsn  4731  preq12b  4781  elinxp  5929  ssrnres  6081  ordtr2  6310  elunirn  7124  fnoprabg  7397  tz7.49  8276  omord  8399  ficard  10321  fpwwe2lem11  10397  1idpr  10785  xrsupsslem  13041  xrinfmsslem  13042  fzospliti  13419  sqrt2irr  15958  algcvga  16284  prmind2  16390  infpn2  16614  grpinveu  18614  1stcrest  22604  fgss2  23025  fgcl  23029  filufint  23071  metrest  23680  reconnlem2  23990  plydivex  25457  ftalem3  26224  chtub  26360  lgsqrmodndvds  26501  2sqlem10  26576  dchrisum0flb  26658  pntpbnd1  26734  clwwlkn1loopb  28407  2pthfrgrrn2  28647  grpoidinvlem3  28868  grpoinveu  28881  elim2ifim  30888  iocinif  31102  qsxpid  31558  tpr2rico  31862  bnj168  32709  dfon2lem8  33766  nolesgn2o  33874  nosupbnd1lem4  33914  noinfbnd1lem4  33929  noetalem1  33944  nn0prpwlem  34511  bj-opelidres  35332  difunieq  35545  voliunnfl  35821  dalem20  37707  elpaddn0  37814  cdleme25a  38367  cdleme29ex  38388  cdlemefr29exN  38416  dibglbN  39180  dihlsscpre  39248  lcfl7N  39515  mapdh9a  39803  mapdh9aOLDN  39804  hdmap11lem2  39856  rtprmirr  40347  sqrtcval  41249  ax6e2eq  42177  eliin2f  42654  itschlc0xyqsol1  46112  mpbiran3d  46142