Theorem ancld 550

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 512	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 206  df-an 396

This theorem is referenced by:  dfmoeu  2536  mopick2  2639  2eu6  2658  cgsexg  3464  cgsex2g  3465  cgsex4g  3466  cgsex4gOLD  3467  ss2abdv  3993  reximdva0  4282  difsn  4728  preq12b  4778  elinxp  5918  ssrnres  6070  ordtr2  6295  elunirn  7106  fnoprabg  7375  tz7.49  8246  omord  8361  dftrpred3g  9412  ficard  10252  fpwwe2lem11  10328  1idpr  10716  xrsupsslem  12970  xrinfmsslem  12971  fzospliti  13347  sqrt2irr  15886  algcvga  16212  prmind2  16318  infpn2  16542  grpinveu  18529  1stcrest  22512  fgss2  22933  fgcl  22937  filufint  22979  metrest  23586  reconnlem2  23896  plydivex  25362  ftalem3  26129  chtub  26265  lgsqrmodndvds  26406  2sqlem10  26481  dchrisum0flb  26563  pntpbnd1  26639  clwwlkn1loopb  28308  2pthfrgrrn2  28548  grpoidinvlem3  28769  grpoinveu  28782  elim2ifim  30789  iocinif  31004  qsxpid  31460  tpr2rico  31764  bnj168  32609  dfon2lem8  33672  nolesgn2o  33801  nosupbnd1lem4  33841  noinfbnd1lem4  33856  noetalem1  33871  nn0prpwlem  34438  bj-opelidres  35259  difunieq  35472  voliunnfl  35748  dalem20  37634  elpaddn0  37741  cdleme25a  38294  cdleme29ex  38315  cdlemefr29exN  38343  dibglbN  39107  dihlsscpre  39175  lcfl7N  39442  mapdh9a  39730  mapdh9aOLDN  39731  hdmap11lem2  39783  rtprmirr  40268  sqrtcval  41138  ax6e2eq  42066  eliin2f  42543  itschlc0xyqsol1  46000  mpbiran3d  46030