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  2529  mopick2  2630  2eu6  2650  cgsexg  3489  cgsex2g  3490  cgsex4g  3491  cgsex4gOLD  3492  reximdva0  4314  difsn  4758  preq12b  4810  elinxp  5979  ssrnres  6139  ordtr2  6365  elunirn  7207  fnoprabg  7492  tz7.49  8390  omord  8509  ficard  10494  fpwwe2lem11  10570  1idpr  10958  xrsupsslem  13243  xrinfmsslem  13244  fzospliti  13628  sqrt2irr  16193  algcvga  16525  prmind2  16631  infpn2  16860  grpinveu  18882  1stcrest  23316  fgss2  23737  fgcl  23741  filufint  23783  metrest  24388  reconnlem2  24692  plydivex  26181  rtprmirr  26646  ftalem3  26961  chtub  27099  lgsqrmodndvds  27240  2sqlem10  27315  dchrisum0flb  27397  pntpbnd1  27473  nolesgn2o  27559  nosupbnd1lem4  27599  noinfbnd1lem4  27614  noetalem1  27629  clwwlkn1loopb  29945  2pthfrgrrn2  30185  grpoidinvlem3  30408  grpoinveu  30421  elim2ifim  32447  iocinif  32677  qsxpid  33306  tpr2rico  33875  bnj168  34693  ellcsrspsn  35601  dfon2lem8  35751  nn0prpwlem  36283  bj-opelidres  37122  difunieq  37335  voliunnfl  37631  dalem20  39660  elpaddn0  39767  cdleme25a  40320  cdleme29ex  40341  cdlemefr29exN  40369  dibglbN  41133  dihlsscpre  41201  lcfl7N  41468  mapdh9a  41756  mapdh9aOLDN  41757  hdmap11lem2  41809  eu6w  42637  sqrtcval  43603  ax6e2eq  44520  eliin2f  45071  clnbgr3stgrgrlic  47984  itschlc0xyqsol1  48728  mpbiran3d  48758