Theorem ancld 560

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 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜓))
2		ancld.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	jcad 522	1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  dfmoeu  2563  mopick2  2665  2eu6  2684  cgsexg  3498  cgsex2g  3499  cgsex4g  3500  reximdva0  4306  difsn  4763  preq12b  4810  elrelb  5784  elinxp  6026  ssrnres  6188  ordtr2  6434  elunirn  7286  fnoprabg  7574  tz7.49  8493  omord  8614  ficard  10688  fpwwe2lem11  10765  1idpr  11153  xrsupsslem  13477  xrinfmsslem  13478  fzospliti  13866  sqrt2irr  16461  algcvga  16798  prmind2  16904  infpn2  17135  grpinveu  19235  qsxpid  19437  1stcrest  23826  fgss2  24248  fgcl  24252  filufint  24294  metrest  24898  reconnlem2  25202  plydivex  26673  rtprmirr  27145  ftalem3  27459  chtub  27596  lgsqrmodndvds  27737  2sqlem10  27812  dchrisum0flb  27894  pntpbnd1  27970  nolesgn2o  28085  nosupbnd1lem4  28125  noinfbnd1lem4  28140  noetalem1  28155  clwwlkn1loopb  30691  2pthfrgrrn2  30941  grpoidinvlem3  31165  grpoinveu  31178  elim2ifim  33239  iocinif  33469  tpr2rico  34655  bnj168  35472  karddom  35970  kardsdom  35971  ellcsrspsn  36614  dfon2lem8  36767  nn0prpwlem  37325  cgsex2gd  38329  bj-opelidres  38350  difunieq  38565  voliunnfl  38850  dalem20  41016  elpaddn0  41123  cdleme25a  41676  cdleme29ex  41697  cdlemefr29exN  41725  dibglbN  42489  dihlsscpre  42557  lcfl7N  42824  mapdh9a  43112  mapdh9aOLDN  43113  hdmap11lem2  43165  eu6w  43953  sqrtcval  44902  ax6e2eq  45800  eliin2f  46392  clnbgr3stgrgrlic  49391  itschlc0xyqsol1  50209  mpbiran3d  50238