Theorem ancld 552

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 514	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:  dfmoeu  2531  mopick2  2634  2eu6  2653  cgsexg  3519  cgsex2g  3520  cgsex4g  3521  cgsex4gOLD  3522  cgsex4gOLDOLD  3523  ss2abdv  4060  reximdva0  4351  difsn  4801  preq12b  4851  elinxp  6018  ssrnres  6175  ordtr2  6406  elunirn  7247  fnoprabg  7528  tz7.49  8442  omord  8565  ficard  10557  fpwwe2lem11  10633  1idpr  11021  xrsupsslem  13283  xrinfmsslem  13284  fzospliti  13661  sqrt2irr  16189  algcvga  16513  prmind2  16619  infpn2  16843  grpinveu  18856  1stcrest  22949  fgss2  23370  fgcl  23374  filufint  23416  metrest  24025  reconnlem2  24335  plydivex  25802  ftalem3  26569  chtub  26705  lgsqrmodndvds  26846  2sqlem10  26921  dchrisum0flb  27003  pntpbnd1  27079  nolesgn2o  27164  nosupbnd1lem4  27204  noinfbnd1lem4  27219  noetalem1  27234  clwwlkn1loopb  29286  2pthfrgrrn2  29526  grpoidinvlem3  29747  grpoinveu  29760  elim2ifim  31765  iocinif  31980  qsxpid  32463  tpr2rico  32881  bnj168  33730  dfon2lem8  34751  nn0prpwlem  35196  bj-opelidres  36031  difunieq  36244  voliunnfl  36521  dalem20  38553  elpaddn0  38660  cdleme25a  39213  cdleme29ex  39234  cdlemefr29exN  39262  dibglbN  40026  dihlsscpre  40094  lcfl7N  40361  mapdh9a  40649  mapdh9aOLDN  40650  hdmap11lem2  40702  rtprmirr  41234  sqrtcval  42378  ax6e2eq  43304  eliin2f  43779  itschlc0xyqsol1  47406  mpbiran3d  47436