Theorem ancld 555

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 517	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 208  df-an 397

This theorem is referenced by:  dfmoeu  2539  mopick2  2641  2eu6  2660  cgsexg  3475  cgsex2g  3476  cgsex4g  3477  reximdva0  4283  difsn  4731  preq12b  4781  elinxp  5971  ssrnres  6129  ordtr2  6355  elunirn  7195  fnoprabg  7479  tz7.49  8374  omord  8493  ficard  10478  fpwwe2lem11  10555  1idpr  10943  xrsupsslem  13250  xrinfmsslem  13251  fzospliti  13637  sqrt2irr  16207  algcvga  16539  prmind2  16645  infpn2  16875  grpinveu  18941  1stcrest  23436  fgss2  23857  fgcl  23861  filufint  23903  metrest  24507  reconnlem2  24811  plydivex  26281  rtprmirr  26742  ftalem3  27056  chtub  27193  lgsqrmodndvds  27334  2sqlem10  27409  dchrisum0flb  27491  pntpbnd1  27567  nolesgn2o  27653  nosupbnd1lem4  27693  noinfbnd1lem4  27708  noetalem1  27723  clwwlkn1loopb  30131  2pthfrgrrn2  30371  grpoidinvlem3  30595  grpoinveu  30608  elim2ifim  32633  iocinif  32873  qsxpid  33445  tpr2rico  34096  bnj168  34913  ellcsrspsn  35869  dfon2lem8  36016  nn0prpwlem  36550  cgsex2gd  37497  bj-opelidres  37521  difunieq  37736  voliunnfl  38031  dalem20  40185  elpaddn0  40292  cdleme25a  40845  cdleme29ex  40866  cdlemefr29exN  40894  dibglbN  41658  dihlsscpre  41726  lcfl7N  41993  mapdh9a  42281  mapdh9aOLDN  42282  hdmap11lem2  42334  eu6w  43126  sqrtcval  44085  ax6e2eq  45001  eliin2f  45551  clnbgr3stgrgrlic  48511  itschlc0xyqsol1  49257  mpbiran3d  49287