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  2522  mopick2  2625  2eu6  2644  cgsexg  3511  cgsex2g  3512  cgsex4g  3513  cgsex4gOLD  3514  cgsex4gOLDOLD  3515  ss2abdv  4052  reximdva0  4343  difsn  4793  preq12b  4843  elinxp  6009  ssrnres  6167  ordtr2  6398  elunirn  7242  fnoprabg  7523  tz7.49  8440  omord  8563  ficard  10556  fpwwe2lem11  10632  1idpr  11020  xrsupsslem  13283  xrinfmsslem  13284  fzospliti  13661  sqrt2irr  16189  algcvga  16513  prmind2  16619  infpn2  16845  grpinveu  18894  1stcrest  23279  fgss2  23700  fgcl  23704  filufint  23746  metrest  24355  reconnlem2  24665  plydivex  26151  ftalem3  26923  chtub  27061  lgsqrmodndvds  27202  2sqlem10  27277  dchrisum0flb  27359  pntpbnd1  27435  nolesgn2o  27520  nosupbnd1lem4  27560  noinfbnd1lem4  27575  noetalem1  27590  clwwlkn1loopb  29765  2pthfrgrrn2  30005  grpoidinvlem3  30228  grpoinveu  30241  elim2ifim  32246  iocinif  32461  qsxpid  32944  tpr2rico  33381  bnj168  34230  dfon2lem8  35257  nn0prpwlem  35697  bj-opelidres  36532  difunieq  36745  voliunnfl  37022  dalem20  39054  elpaddn0  39161  cdleme25a  39714  cdleme29ex  39735  cdlemefr29exN  39763  dibglbN  40527  dihlsscpre  40595  lcfl7N  40862  mapdh9a  41150  mapdh9aOLDN  41151  hdmap11lem2  41203  rtprmirr  41726  sqrtcval  42881  ax6e2eq  43807  eliin2f  44281  itschlc0xyqsol1  47640  mpbiran3d  47670