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  2637  2eu6  2657  cgsexg  3526  cgsex2g  3527  cgsex4g  3528  cgsex4gOLD  3529  reximdva0  4355  difsn  4798  preq12b  4850  elinxp  6037  ssrnres  6198  ordtr2  6428  elunirn  7271  fnoprabg  7556  tz7.49  8485  omord  8606  ficard  10605  fpwwe2lem11  10681  1idpr  11069  xrsupsslem  13349  xrinfmsslem  13350  fzospliti  13731  sqrt2irr  16285  algcvga  16616  prmind2  16722  infpn2  16951  grpinveu  18992  1stcrest  23461  fgss2  23882  fgcl  23886  filufint  23928  metrest  24537  reconnlem2  24849  plydivex  26339  rtprmirr  26803  ftalem3  27118  chtub  27256  lgsqrmodndvds  27397  2sqlem10  27472  dchrisum0flb  27554  pntpbnd1  27630  nolesgn2o  27716  nosupbnd1lem4  27756  noinfbnd1lem4  27771  noetalem1  27786  clwwlkn1loopb  30062  2pthfrgrrn2  30302  grpoidinvlem3  30525  grpoinveu  30538  elim2ifim  32558  iocinif  32783  qsxpid  33390  tpr2rico  33911  bnj168  34744  ellcsrspsn  35646  dfon2lem8  35791  nn0prpwlem  36323  bj-opelidres  37162  difunieq  37375  voliunnfl  37671  dalem20  39695  elpaddn0  39802  cdleme25a  40355  cdleme29ex  40376  cdlemefr29exN  40404  dibglbN  41168  dihlsscpre  41236  lcfl7N  41503  mapdh9a  41791  mapdh9aOLDN  41792  hdmap11lem2  41844  eu6w  42686  sqrtcval  43654  ax6e2eq  44577  eliin2f  45109  clnbgr3stgrgrlic  47979  itschlc0xyqsol1  48687  mpbiran3d  48717