Theorem ancld 559

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 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜓))
2		ancld.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	jcad 521	1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  dfmoeu  2563  mopick2  2665  2eu6  2684  cgsexg  3499  cgsex2g  3500  cgsex4g  3501  reximdva0  4310  difsn  4766  preq12b  4815  elinxp  6018  ssrnres  6176  ordtr2  6406  elunirn  7249  fnoprabg  7533  tz7.49  8428  omord  8549  ficard  10544  fpwwe2lem11  10621  1idpr  11009  xrsupsslem  13328  xrinfmsslem  13329  fzospliti  13716  sqrt2irr  16300  algcvga  16632  prmind2  16738  infpn2  16968  grpinveu  19036  qsxpid  19238  1stcrest  23610  fgss2  24031  fgcl  24035  filufint  24077  metrest  24681  reconnlem2  24985  plydivex  26458  rtprmirr  26925  ftalem3  27239  chtub  27376  lgsqrmodndvds  27517  2sqlem10  27592  dchrisum0flb  27674  pntpbnd1  27750  nolesgn2o  27835  nosupbnd1lem4  27875  noinfbnd1lem4  27890  noetalem1  27905  clwwlkn1loopb  30394  2pthfrgrrn2  30634  grpoidinvlem3  30858  grpoinveu  30871  elim2ifim  32891  iocinif  33126  tpr2rico  34302  bnj168  35119  karddom  35574  kardsdom  35575  ellcsrspsn  36133  dfon2lem8  36280  nn0prpwlem  36833  cgsex2gd  37781  bj-opelidres  37805  difunieq  38020  voliunnfl  38315  dalem20  40467  elpaddn0  40574  cdleme25a  41127  cdleme29ex  41148  cdlemefr29exN  41176  dibglbN  41940  dihlsscpre  42008  lcfl7N  42275  mapdh9a  42563  mapdh9aOLDN  42564  hdmap11lem2  42616  eu6w  43408  sqrtcval  44367  ax6e2eq  45266  eliin2f  45822  clnbgr3stgrgrlic  48785  itschlc0xyqsol1  49546  mpbiran3d  49575