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  2560  mopick2  2662  2eu6  2681  cgsexg  3494  cgsex2g  3495  cgsex4g  3496  reximdva0  4302  difsn  4757  preq12b  4804  elrelb  5776  elinxp  6010  ssrnres  6172  ordtr2  6411  elunirn  7259  fnoprabg  7547  tz7.49  8462  omord  8583  ficard  10656  fpwwe2lem11  10733  1idpr  11121  xrsupsslem  13444  xrinfmsslem  13445  fzospliti  13833  sqrt2irr  16426  algcvga  16763  prmind2  16869  infpn2  17100  grpinveu  19194  qsxpid  19396  1stcrest  23780  fgss2  24202  fgcl  24206  filufint  24248  metrest  24852  reconnlem2  25156  plydivex  26627  rtprmirr  27097  ftalem3  27411  chtub  27548  lgsqrmodndvds  27689  2sqlem10  27764  dchrisum0flb  27846  pntpbnd1  27922  nolesgn2o  28037  nosupbnd1lem4  28077  noinfbnd1lem4  28092  noetalem1  28107  clwwlkn1loopb  30643  2pthfrgrrn2  30893  grpoidinvlem3  31117  grpoinveu  31130  elim2ifim  33192  iocinif  33423  tpr2rico  34594  bnj168  35411  karddom  35889  kardsdom  35890  ellcsrspsn  36496  dfon2lem8  36648  nn0prpwlem  37206  cgsex2gd  38167  bj-opelidres  38191  difunieq  38406  voliunnfl  38691  dalem20  40859  elpaddn0  40966  cdleme25a  41519  cdleme29ex  41540  cdlemefr29exN  41568  dibglbN  42332  dihlsscpre  42400  lcfl7N  42667  mapdh9a  42955  mapdh9aOLDN  42956  hdmap11lem2  43008  eu6w  43796  sqrtcval  44750  ax6e2eq  45648  eliin2f  46227  clnbgr3stgrgrlic  49226  itschlc0xyqsol1  49986  mpbiran3d  50015