Theorem ancld 552

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  dfmoeu  2531  mopick2  2634  2eu6  2653  cgsexg  3519  cgsex2g  3520  cgsex4g  3521  cgsex4gOLD  3522  cgsex4gOLDOLD  3523  ss2abdv  4061  reximdva0  4352  difsn  4802  preq12b  4852  elinxp  6020  ssrnres  6178  ordtr2  6409  elunirn  7250  fnoprabg  7531  tz7.49  8445  omord  8568  ficard  10560  fpwwe2lem11  10636  1idpr  11024  xrsupsslem  13286  xrinfmsslem  13287  fzospliti  13664  sqrt2irr  16192  algcvga  16516  prmind2  16622  infpn2  16846  grpinveu  18859  1stcrest  22957  fgss2  23378  fgcl  23382  filufint  23424  metrest  24033  reconnlem2  24343  plydivex  25810  ftalem3  26579  chtub  26715  lgsqrmodndvds  26856  2sqlem10  26931  dchrisum0flb  27013  pntpbnd1  27089  nolesgn2o  27174  nosupbnd1lem4  27214  noinfbnd1lem4  27229  noetalem1  27244  clwwlkn1loopb  29296  2pthfrgrrn2  29536  grpoidinvlem3  29759  grpoinveu  29772  elim2ifim  31777  iocinif  31992  qsxpid  32474  tpr2rico  32892  bnj168  33741  dfon2lem8  34762  nn0prpwlem  35207  bj-opelidres  36042  difunieq  36255  voliunnfl  36532  dalem20  38564  elpaddn0  38671  cdleme25a  39224  cdleme29ex  39245  cdlemefr29exN  39273  dibglbN  40037  dihlsscpre  40105  lcfl7N  40372  mapdh9a  40660  mapdh9aOLDN  40661  hdmap11lem2  40713  rtprmirr  41237  sqrtcval  42392  ax6e2eq  43318  eliin2f  43793  itschlc0xyqsol1  47452  mpbiran3d  47482