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  4303  difsn  4761  preq12b  4810  elinxp  6012  ssrnres  6171  ordtr2  6403  elunirn  7248  fnoprabg  7536  tz7.49  8434  omord  8555  ficard  10573  fpwwe2lem11  10650  1idpr  11038  xrsupsslem  13359  xrinfmsslem  13360  fzospliti  13747  sqrt2irr  16337  algcvga  16669  prmind2  16775  infpn2  17005  grpinveu  19098  qsxpid  19300  1stcrest  23678  fgss2  24100  fgcl  24104  filufint  24146  metrest  24750  reconnlem2  25054  plydivex  26527  rtprmirr  26997  ftalem3  27311  chtub  27448  lgsqrmodndvds  27589  2sqlem10  27664  dchrisum0flb  27746  pntpbnd1  27822  nolesgn2o  27907  nosupbnd1lem4  27947  noinfbnd1lem4  27962  noetalem1  27977  clwwlkn1loopb  30513  2pthfrgrrn2  30763  grpoidinvlem3  30987  grpoinveu  31000  elim2ifim  33020  iocinif  33252  tpr2rico  34422  bnj168  35240  karddom  35687  kardsdom  35688  ellcsrspsn  36220  dfon2lem8  36367  nn0prpwlem  36941  cgsex2gd  37889  bj-opelidres  37913  difunieq  38128  voliunnfl  38413  dalem20  40566  elpaddn0  40673  cdleme25a  41226  cdleme29ex  41247  cdlemefr29exN  41275  dibglbN  42039  dihlsscpre  42107  lcfl7N  42374  mapdh9a  42662  mapdh9aOLDN  42663  hdmap11lem2  42715  eu6w  43522  sqrtcval  44481  ax6e2eq  45380  eliin2f  45936  clnbgr3stgrgrlic  48936  itschlc0xyqsol1  49696  mpbiran3d  49725