Theorem ancld 550

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  dfmoeu  2529  mopick2  2630  2eu6  2650  cgsexg  3483  cgsex2g  3484  cgsex4g  3485  cgsex4gOLD  3486  reximdva0  4308  difsn  4752  preq12b  4804  elinxp  5974  ssrnres  6131  ordtr2  6356  elunirn  7191  fnoprabg  7476  tz7.49  8374  omord  8493  ficard  10478  fpwwe2lem11  10554  1idpr  10942  xrsupsslem  13228  xrinfmsslem  13229  fzospliti  13613  sqrt2irr  16177  algcvga  16509  prmind2  16615  infpn2  16844  grpinveu  18872  1stcrest  23357  fgss2  23778  fgcl  23782  filufint  23824  metrest  24429  reconnlem2  24733  plydivex  26222  rtprmirr  26687  ftalem3  27002  chtub  27140  lgsqrmodndvds  27281  2sqlem10  27356  dchrisum0flb  27438  pntpbnd1  27514  nolesgn2o  27600  nosupbnd1lem4  27640  noinfbnd1lem4  27655  noetalem1  27670  clwwlkn1loopb  30006  2pthfrgrrn2  30246  grpoidinvlem3  30469  grpoinveu  30482  elim2ifim  32508  iocinif  32743  qsxpid  33318  tpr2rico  33898  bnj168  34716  ellcsrspsn  35633  dfon2lem8  35783  nn0prpwlem  36315  bj-opelidres  37154  difunieq  37367  voliunnfl  37663  dalem20  39692  elpaddn0  39799  cdleme25a  40352  cdleme29ex  40373  cdlemefr29exN  40401  dibglbN  41165  dihlsscpre  41233  lcfl7N  41500  mapdh9a  41788  mapdh9aOLDN  41789  hdmap11lem2  41841  eu6w  42669  sqrtcval  43634  ax6e2eq  44551  eliin2f  45102  clnbgr3stgrgrlic  48024  itschlc0xyqsol1  48771  mpbiran3d  48801