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  2536  mopick2  2638  2eu6  2658  cgsexg  3475  cgsex2g  3476  cgsex4g  3477  reximdva0  4296  difsn  4742  preq12b  4794  elinxp  5978  ssrnres  6136  ordtr2  6362  elunirn  7199  fnoprabg  7483  tz7.49  8377  omord  8496  ficard  10478  fpwwe2lem11  10555  1idpr  10943  xrsupsslem  13250  xrinfmsslem  13251  fzospliti  13637  sqrt2irr  16207  algcvga  16539  prmind2  16645  infpn2  16875  grpinveu  18941  1stcrest  23428  fgss2  23849  fgcl  23853  filufint  23895  metrest  24499  reconnlem2  24803  plydivex  26274  rtprmirr  26737  ftalem3  27052  chtub  27189  lgsqrmodndvds  27330  2sqlem10  27405  dchrisum0flb  27487  pntpbnd1  27563  nolesgn2o  27649  nosupbnd1lem4  27689  noinfbnd1lem4  27704  noetalem1  27719  clwwlkn1loopb  30128  2pthfrgrrn2  30368  grpoidinvlem3  30592  grpoinveu  30605  elim2ifim  32630  iocinif  32869  qsxpid  33437  tpr2rico  34072  bnj168  34889  ellcsrspsn  35839  dfon2lem8  35986  nn0prpwlem  36520  cgsex2gd  37467  bj-opelidres  37491  difunieq  37704  voliunnfl  37999  dalem20  40153  elpaddn0  40260  cdleme25a  40813  cdleme29ex  40834  cdlemefr29exN  40862  dibglbN  41626  dihlsscpre  41694  lcfl7N  41961  mapdh9a  42249  mapdh9aOLDN  42250  hdmap11lem2  42302  eu6w  43123  sqrtcval  44086  ax6e2eq  45002  eliin2f  45552  clnbgr3stgrgrlic  48508  itschlc0xyqsol1  49254  mpbiran3d  49284