Theorem ancld 575

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  equvinv  2003  mo2v  2505  mopick2  2569  2eu6  2587  cgsexg  3269  cgsex2g  3270  cgsex4g  3271  reximdva0  3966  difsn  4360  preq12b  4413  elres  5470  relssres  5472  ordtr2  5806  elunirn  6549  fnoprabg  6803  tz7.49  7585  omord  7693  ficard  9425  fpwwe2lem12  9501  1idpr  9889  xrsupsslem  12175  xrinfmsslem  12176  fzospliti  12539  sqrt2irr  15023  algcvga  15339  prmind2  15445  infpn2  15664  grpinveu  17503  1stcrest  21304  fgss2  21725  fgcl  21729  filufint  21771  metrest  22376  reconnlem2  22677  plydivex  24097  ftalem3  24846  chtub  24982  lgsqrmodndvds  25123  2sqlem10  25198  dchrisum0flb  25244  pntpbnd1  25320  clwwlkn1loopb  27006  2pthfrgrrn2  27263  grpoidinvlem3  27488  grpoinveu  27501  elim2ifim  29490  iocinif  29671  tpr2rico  30086  bnj168  30924  dfon2lem8  31819  dftrpred3g  31857  nolesgn2o  31949  nosupbnd1lem4  31982  nn0prpwlem  32442  voliunnfl  33583  dalem20  35297  elpaddn0  35404  cdleme25a  35958  cdleme29ex  35979  cdlemefr29exN  36007  dibglbN  36772  dihlsscpre  36840  lcfl7N  37107  mapdh9a  37396  mapdh9aOLDN  37397  hdmap11lem2  37451  ax6e2eq  39090  eliin2f  39601