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  2565  mopick2  2667  2eu6  2686  cgsexg  3501  cgsex2g  3502  cgsex4g  3503  reximdva0  4310  difsn  4768  preq12b  4817  elinxp  6020  ssrnres  6178  ordtr2  6410  elunirn  7254  fnoprabg  7542  tz7.49  8438  omord  8559  ficard  10564  fpwwe2lem11  10641  1idpr  11029  xrsupsslem  13349  xrinfmsslem  13350  fzospliti  13737  sqrt2irr  16327  algcvga  16659  prmind2  16765  infpn2  16995  grpinveu  19085  qsxpid  19287  1stcrest  23660  fgss2  24082  fgcl  24086  filufint  24128  metrest  24732  reconnlem2  25036  plydivex  26509  rtprmirr  26976  ftalem3  27290  chtub  27427  lgsqrmodndvds  27568  2sqlem10  27643  dchrisum0flb  27725  pntpbnd1  27801  nolesgn2o  27886  nosupbnd1lem4  27926  noinfbnd1lem4  27941  noetalem1  27956  clwwlkn1loopb  30461  2pthfrgrrn2  30705  grpoidinvlem3  30929  grpoinveu  30942  elim2ifim  32962  iocinif  33196  tpr2rico  34366  bnj168  35184  karddom  35631  kardsdom  35632  ellcsrspsn  36170  dfon2lem8  36317  nn0prpwlem  36890  cgsex2gd  37838  bj-opelidres  37862  difunieq  38077  voliunnfl  38372  dalem20  40525  elpaddn0  40632  cdleme25a  41185  cdleme29ex  41206  cdlemefr29exN  41234  dibglbN  41998  dihlsscpre  42066  lcfl7N  42333  mapdh9a  42621  mapdh9aOLDN  42622  hdmap11lem2  42674  eu6w  43466  sqrtcval  44425  ax6e2eq  45324  eliin2f  45880  clnbgr3stgrgrlic  48843  itschlc0xyqsol1  49603  mpbiran3d  49632