Theorem ancld 554

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 516	1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  dfmoeu  2535  mopick2  2638  2eu6  2657  cgsexg  3450  cgsex2g  3451  cgsex4g  3452  cgsex4gOLD  3453  ss2abdv  3977  reximdva0  4266  difsn  4711  preq12b  4761  elinxp  5889  ssrnres  6041  ordtr2  6257  elunirn  7064  fnoprabg  7333  tz7.49  8181  omord  8296  dftrpred3g  9339  ficard  10179  fpwwe2lem11  10255  1idpr  10643  xrsupsslem  12897  xrinfmsslem  12898  fzospliti  13274  sqrt2irr  15810  algcvga  16136  prmind2  16242  infpn2  16466  grpinveu  18402  1stcrest  22350  fgss2  22771  fgcl  22775  filufint  22817  metrest  23422  reconnlem2  23724  plydivex  25190  ftalem3  25957  chtub  26093  lgsqrmodndvds  26234  2sqlem10  26309  dchrisum0flb  26391  pntpbnd1  26467  clwwlkn1loopb  28126  2pthfrgrrn2  28366  grpoidinvlem3  28587  grpoinveu  28600  elim2ifim  30607  iocinif  30822  qsxpid  31272  tpr2rico  31576  bnj168  32421  dfon2lem8  33485  nolesgn2o  33611  nosupbnd1lem4  33651  noinfbnd1lem4  33666  noetalem1  33681  nn0prpwlem  34248  bj-opelidres  35067  difunieq  35282  voliunnfl  35558  dalem20  37444  elpaddn0  37551  cdleme25a  38104  cdleme29ex  38125  cdlemefr29exN  38153  dibglbN  38917  dihlsscpre  38985  lcfl7N  39252  mapdh9a  39540  mapdh9aOLDN  39541  hdmap11lem2  39593  rtprmirr  40055  sqrtcval  40925  ax6e2eq  41850  eliin2f  42327  itschlc0xyqsol1  45785  mpbiran3d  45815