Theorem ancld 543

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  dfmoeu  2547  mopick2  2675  2eu6  2697  cgsexg  3460  cgsex2g  3461  cgsex4g  3462  reximdva0  4201  difsn  4610  preq12b  4660  elinxp  5740  ssrnres  5880  ordtr2  6078  elunirn  6841  fnoprabg  7097  tz7.49  7890  omord  8001  ficard  9791  fpwwe2lem12  9867  1idpr  10255  xrsupsslem  12522  xrinfmsslem  12523  fzospliti  12890  sqrt2irr  15468  algcvga  15785  prmind2  15891  infpn2  16111  grpinveu  17937  1stcrest  21780  fgss2  22201  fgcl  22205  filufint  22247  metrest  22852  reconnlem2  23153  plydivex  24604  ftalem3  25369  chtub  25505  lgsqrmodndvds  25646  2sqlem10  25721  dchrisum0flb  25803  pntpbnd1  25879  clwwlkn1loopb  27574  2pthfrgrrn2  27832  grpoidinvlem3  28075  grpoinveu  28088  elim2ifim  30085  iocinif  30280  tpr2rico  30831  bnj168  31680  dfon2lem8  32595  dftrpred3g  32633  nolesgn2o  32739  nosupbnd1lem4  32772  nn0prpwlem  33231  difunieq  34137  voliunnfl  34417  dalem20  36314  elpaddn0  36421  cdleme25a  36974  cdleme29ex  36995  cdlemefr29exN  37023  dibglbN  37787  dihlsscpre  37855  lcfl7N  38122  mapdh9a  38410  mapdh9aOLDN  38411  hdmap11lem2  38463  rtprmirr  38667  ax6e2eq  40350  eliin2f  40831  itschlc0xyqsol1  44156