Theorem ancld 576

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

Syntax hints:   → wi 4   ∧ wa 384

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 386

This theorem is referenced by:  equvinv  1959  equvinivOLD  1961  mo2v  2477  mopick2  2540  2eu6  2558  cgsexg  3238  cgsex2g  3239  cgsex4g  3240  reximdva0  3933  difsn  4328  preq12b  4382  elres  5435  relssres  5437  ordtr2  5768  elunirn  6509  fnoprabg  6761  tz7.49  7540  omord  7648  ficard  9387  fpwwe2lem12  9463  1idpr  9851  xrsupsslem  12137  xrinfmsslem  12138  fzospliti  12500  sqrt2irr  14979  algcvga  15292  prmind2  15398  infpn2  15617  grpinveu  17456  1stcrest  21256  fgss2  21678  fgcl  21682  filufint  21724  metrest  22329  reconnlem2  22630  plydivex  24052  ftalem3  24801  chtub  24937  lgsqrmodndvds  25078  2sqlem10  25153  dchrisum0flb  25199  pntpbnd1  25275  2pthfrgrrn2  27147  grpoidinvlem3  27360  grpoinveu  27373  elim2ifim  29364  iocinif  29543  tpr2rico  29958  bnj168  30798  dfon2lem8  31695  dftrpred3g  31733  nolesgn2o  31824  nosupbnd1lem4  31857  nn0prpwlem  32317  voliunnfl  33453  dalem20  34979  elpaddn0  35086  cdleme25a  35641  cdleme29ex  35662  cdlemefr29exN  35690  dibglbN  36455  dihlsscpre  36523  lcfl7N  36790  mapdh9a  37079  mapdh9aOLDN  37080  hdmap11lem2  37134  ax6e2eq  38773  eliin2f  39287