Theorem ancld 559

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 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜓))
2		ancld.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	jcad 521	1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  dfmoeu  2569  mopick2  2671  2eu6  2690  cgsexg  3507  cgsex2g  3508  cgsex4g  3509  reximdva0  4317  difsn  4767  preq12b  4816  elinxp  6016  ssrnres  6174  ordtr2  6404  elunirn  7247  fnoprabg  7531  tz7.49  8428  omord  8549  ficard  10545  fpwwe2lem11  10622  1idpr  11010  xrsupsslem  13329  xrinfmsslem  13330  fzospliti  13716  sqrt2irr  16301  algcvga  16633  prmind2  16739  infpn2  16969  grpinveu  19037  qsxpid  19239  1stcrest  23575  fgss2  23996  fgcl  24000  filufint  24042  metrest  24646  reconnlem2  24950  plydivex  26423  rtprmirr  26887  ftalem3  27201  chtub  27338  lgsqrmodndvds  27479  2sqlem10  27554  dchrisum0flb  27636  pntpbnd1  27712  nolesgn2o  27797  nosupbnd1lem4  27837  noinfbnd1lem4  27852  noetalem1  27867  clwwlkn1loopb  30331  2pthfrgrrn2  30571  grpoidinvlem3  30795  grpoinveu  30808  elim2ifim  32828  iocinif  33063  tpr2rico  34243  bnj168  35060  ellcsrspsn  36028  dfon2lem8  36175  nn0prpwlem  36718  cgsex2gd  37664  bj-opelidres  37688  difunieq  37903  voliunnfl  38198  dalem20  40352  elpaddn0  40459  cdleme25a  41012  cdleme29ex  41033  cdlemefr29exN  41061  dibglbN  41825  dihlsscpre  41893  lcfl7N  42160  mapdh9a  42448  mapdh9aOLDN  42449  hdmap11lem2  42501  eu6w  43295  sqrtcval  44254  ax6e2eq  45153  eliin2f  45709  clnbgr3stgrgrlic  48669  itschlc0xyqsol1  49426  mpbiran3d  49455