Theorem ancld 558

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 520	1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  dfmoeu  2561  mopick2  2663  2eu6  2682  cgsexg  3497  cgsex2g  3498  cgsex4g  3499  reximdva0  4305  difsn  4755  preq12b  4805  elinxp  6001  ssrnres  6159  ordtr2  6386  elunirn  7230  fnoprabg  7514  tz7.49  8410  omord  8531  ficard  10516  fpwwe2lem11  10593  1idpr  10981  xrsupsslem  13304  xrinfmsslem  13305  fzospliti  13691  sqrt2irr  16272  algcvga  16604  prmind2  16710  infpn2  16940  grpinveu  19007  1stcrest  23501  fgss2  23922  fgcl  23926  filufint  23968  metrest  24572  reconnlem2  24876  plydivex  26349  rtprmirr  26813  ftalem3  27127  chtub  27264  lgsqrmodndvds  27405  2sqlem10  27480  dchrisum0flb  27562  pntpbnd1  27638  nolesgn2o  27723  nosupbnd1lem4  27763  noinfbnd1lem4  27778  noetalem1  27793  clwwlkn1loopb  30202  2pthfrgrrn2  30442  grpoidinvlem3  30666  grpoinveu  30679  elim2ifim  32704  iocinif  32944  qsxpid  33509  tpr2rico  34170  bnj168  34987  ellcsrspsn  35952  dfon2lem8  36099  nn0prpwlem  36643  cgsex2gd  37590  bj-opelidres  37614  difunieq  37829  voliunnfl  38124  dalem20  40278  elpaddn0  40385  cdleme25a  40938  cdleme29ex  40959  cdlemefr29exN  40987  dibglbN  41751  dihlsscpre  41819  lcfl7N  42086  mapdh9a  42374  mapdh9aOLDN  42375  hdmap11lem2  42427  eu6w  43219  sqrtcval  44178  ax6e2eq  45094  eliin2f  45643  clnbgr3stgrgrlic  48603  itschlc0xyqsol1  49349  mpbiran3d  49379