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  2536  mopick2  2638  2eu6  2658  cgsexg  3487  cgsex2g  3488  cgsex4g  3489  cgsex4gOLD  3490  reximdva0  4309  difsn  4756  preq12b  4808  elinxp  5986  ssrnres  6144  ordtr2  6370  elunirn  7207  fnoprabg  7491  tz7.49  8386  omord  8505  ficard  10487  fpwwe2lem11  10564  1idpr  10952  xrsupsslem  13234  xrinfmsslem  13235  fzospliti  13619  sqrt2irr  16186  algcvga  16518  prmind2  16624  infpn2  16853  grpinveu  18916  1stcrest  23409  fgss2  23830  fgcl  23834  filufint  23876  metrest  24480  reconnlem2  24784  plydivex  26273  rtprmirr  26738  ftalem3  27053  chtub  27191  lgsqrmodndvds  27332  2sqlem10  27407  dchrisum0flb  27489  pntpbnd1  27565  nolesgn2o  27651  nosupbnd1lem4  27691  noinfbnd1lem4  27706  noetalem1  27721  clwwlkn1loopb  30130  2pthfrgrrn2  30370  grpoidinvlem3  30594  grpoinveu  30607  elim2ifim  32632  iocinif  32872  qsxpid  33455  tpr2rico  34090  bnj168  34907  ellcsrspsn  35857  dfon2lem8  36004  nn0prpwlem  36538  cgsex2gd  37392  bj-opelidres  37416  difunieq  37629  voliunnfl  37915  dalem20  40069  elpaddn0  40176  cdleme25a  40729  cdleme29ex  40750  cdlemefr29exN  40778  dibglbN  41542  dihlsscpre  41610  lcfl7N  41877  mapdh9a  42165  mapdh9aOLDN  42166  hdmap11lem2  42218  eu6w  43034  sqrtcval  43997  ax6e2eq  44913  eliin2f  45463  clnbgr3stgrgrlic  48380  itschlc0xyqsol1  49126  mpbiran3d  49156