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  2530  mopick2  2631  2eu6  2651  cgsexg  3495  cgsex2g  3496  cgsex4g  3497  cgsex4gOLD  3498  reximdva0  4321  difsn  4765  preq12b  4817  elinxp  5993  ssrnres  6154  ordtr2  6380  elunirn  7228  fnoprabg  7515  tz7.49  8416  omord  8535  ficard  10525  fpwwe2lem11  10601  1idpr  10989  xrsupsslem  13274  xrinfmsslem  13275  fzospliti  13659  sqrt2irr  16224  algcvga  16556  prmind2  16662  infpn2  16891  grpinveu  18913  1stcrest  23347  fgss2  23768  fgcl  23772  filufint  23814  metrest  24419  reconnlem2  24723  plydivex  26212  rtprmirr  26677  ftalem3  26992  chtub  27130  lgsqrmodndvds  27271  2sqlem10  27346  dchrisum0flb  27428  pntpbnd1  27504  nolesgn2o  27590  nosupbnd1lem4  27630  noinfbnd1lem4  27645  noetalem1  27660  clwwlkn1loopb  29979  2pthfrgrrn2  30219  grpoidinvlem3  30442  grpoinveu  30455  elim2ifim  32481  iocinif  32711  qsxpid  33340  tpr2rico  33909  bnj168  34727  ellcsrspsn  35635  dfon2lem8  35785  nn0prpwlem  36317  bj-opelidres  37156  difunieq  37369  voliunnfl  37665  dalem20  39694  elpaddn0  39801  cdleme25a  40354  cdleme29ex  40375  cdlemefr29exN  40403  dibglbN  41167  dihlsscpre  41235  lcfl7N  41502  mapdh9a  41790  mapdh9aOLDN  41791  hdmap11lem2  41843  eu6w  42671  sqrtcval  43637  ax6e2eq  44554  eliin2f  45105  clnbgr3stgrgrlic  48015  itschlc0xyqsol1  48759  mpbiran3d  48789