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  2539  mopick2  2640  2eu6  2660  cgsexg  3536  cgsex2g  3537  cgsex4g  3538  cgsex4gOLD  3539  reximdva0  4378  difsn  4823  preq12b  4875  elinxp  6048  ssrnres  6209  ordtr2  6439  elunirn  7288  fnoprabg  7573  tz7.49  8501  omord  8624  ficard  10634  fpwwe2lem11  10710  1idpr  11098  xrsupsslem  13369  xrinfmsslem  13370  fzospliti  13748  sqrt2irr  16297  algcvga  16626  prmind2  16732  infpn2  16960  grpinveu  19014  1stcrest  23482  fgss2  23903  fgcl  23907  filufint  23949  metrest  24558  reconnlem2  24868  plydivex  26357  rtprmirr  26821  ftalem3  27136  chtub  27274  lgsqrmodndvds  27415  2sqlem10  27490  dchrisum0flb  27572  pntpbnd1  27648  nolesgn2o  27734  nosupbnd1lem4  27774  noinfbnd1lem4  27789  noetalem1  27804  clwwlkn1loopb  30075  2pthfrgrrn2  30315  grpoidinvlem3  30538  grpoinveu  30551  elim2ifim  32568  iocinif  32786  qsxpid  33355  tpr2rico  33858  bnj168  34706  ellcsrspsn  35609  dfon2lem8  35754  nn0prpwlem  36288  bj-opelidres  37127  difunieq  37340  voliunnfl  37624  dalem20  39650  elpaddn0  39757  cdleme25a  40310  cdleme29ex  40331  cdlemefr29exN  40359  dibglbN  41123  dihlsscpre  41191  lcfl7N  41458  mapdh9a  41746  mapdh9aOLDN  41747  hdmap11lem2  41799  eu6w  42631  sqrtcval  43603  ax6e2eq  44528  eliin2f  45006  itschlc0xyqsol1  48500  mpbiran3d  48530