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  3492  cgsex2g  3493  cgsex4g  3494  cgsex4gOLD  3495  reximdva0  4318  difsn  4762  preq12b  4814  elinxp  5990  ssrnres  6151  ordtr2  6377  elunirn  7225  fnoprabg  7512  tz7.49  8413  omord  8532  ficard  10518  fpwwe2lem11  10594  1idpr  10982  xrsupsslem  13267  xrinfmsslem  13268  fzospliti  13652  sqrt2irr  16217  algcvga  16549  prmind2  16655  infpn2  16884  grpinveu  18906  1stcrest  23340  fgss2  23761  fgcl  23765  filufint  23807  metrest  24412  reconnlem2  24716  plydivex  26205  rtprmirr  26670  ftalem3  26985  chtub  27123  lgsqrmodndvds  27264  2sqlem10  27339  dchrisum0flb  27421  pntpbnd1  27497  nolesgn2o  27583  nosupbnd1lem4  27623  noinfbnd1lem4  27638  noetalem1  27653  clwwlkn1loopb  29972  2pthfrgrrn2  30212  grpoidinvlem3  30435  grpoinveu  30448  elim2ifim  32474  iocinif  32704  qsxpid  33333  tpr2rico  33902  bnj168  34720  ellcsrspsn  35628  dfon2lem8  35778  nn0prpwlem  36310  bj-opelidres  37149  difunieq  37362  voliunnfl  37658  dalem20  39687  elpaddn0  39794  cdleme25a  40347  cdleme29ex  40368  cdlemefr29exN  40396  dibglbN  41160  dihlsscpre  41228  lcfl7N  41495  mapdh9a  41783  mapdh9aOLDN  41784  hdmap11lem2  41836  eu6w  42664  sqrtcval  43630  ax6e2eq  44547  eliin2f  45098  clnbgr3stgrgrlic  48011  itschlc0xyqsol1  48755  mpbiran3d  48785