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 207  df-an 396

This theorem is referenced by:  dfmoeu  2535  mopick2  2637  2eu6  2657  cgsexg  3474  cgsex2g  3475  cgsex4g  3476  reximdva0  4295  difsn  4743  preq12b  4793  elinxp  5984  ssrnres  6142  ordtr2  6368  elunirn  7206  fnoprabg  7490  tz7.49  8384  omord  8503  ficard  10487  fpwwe2lem11  10564  1idpr  10952  xrsupsslem  13259  xrinfmsslem  13260  fzospliti  13646  sqrt2irr  16216  algcvga  16548  prmind2  16654  infpn2  16884  grpinveu  18950  1stcrest  23418  fgss2  23839  fgcl  23843  filufint  23885  metrest  24489  reconnlem2  24793  plydivex  26263  rtprmirr  26724  ftalem3  27038  chtub  27175  lgsqrmodndvds  27316  2sqlem10  27391  dchrisum0flb  27473  pntpbnd1  27549  nolesgn2o  27635  nosupbnd1lem4  27675  noinfbnd1lem4  27690  noetalem1  27705  clwwlkn1loopb  30113  2pthfrgrrn2  30353  grpoidinvlem3  30577  grpoinveu  30590  elim2ifim  32615  iocinif  32854  qsxpid  33422  tpr2rico  34056  bnj168  34873  ellcsrspsn  35823  dfon2lem8  35970  nn0prpwlem  36504  cgsex2gd  37451  bj-opelidres  37475  difunieq  37690  voliunnfl  37985  dalem20  40139  elpaddn0  40246  cdleme25a  40799  cdleme29ex  40820  cdlemefr29exN  40848  dibglbN  41612  dihlsscpre  41680  lcfl7N  41947  mapdh9a  42235  mapdh9aOLDN  42236  hdmap11lem2  42288  eu6w  43109  sqrtcval  44068  ax6e2eq  44984  eliin2f  45534  clnbgr3stgrgrlic  48496  itschlc0xyqsol1  49242  mpbiran3d  49272