Theorem ancld 553

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

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  dfmoeu  2618  mopick2  2722  2eu6  2742  cgsexg  3537  cgsex2g  3538  cgsex4g  3539  reximdva0  4312  difsn  4731  preq12b  4781  elinxp  5890  ssrnres  6035  ordtr2  6235  elunirn  7010  fnoprabg  7275  tz7.49  8081  omord  8194  ficard  9987  fpwwe2lem12  10063  1idpr  10451  xrsupsslem  12701  xrinfmsslem  12702  fzospliti  13070  sqrt2irr  15602  algcvga  15923  prmind2  16029  infpn2  16249  grpinveu  18138  1stcrest  22061  fgss2  22482  fgcl  22486  filufint  22528  metrest  23134  reconnlem2  23435  plydivex  24886  ftalem3  25652  chtub  25788  lgsqrmodndvds  25929  2sqlem10  26004  dchrisum0flb  26086  pntpbnd1  26162  clwwlkn1loopb  27821  2pthfrgrrn2  28062  grpoidinvlem3  28283  grpoinveu  28296  elim2ifim  30300  iocinif  30504  qsxpid  30927  tpr2rico  31155  bnj168  32000  dfon2lem8  33035  dftrpred3g  33072  nolesgn2o  33178  nosupbnd1lem4  33211  nn0prpwlem  33670  bj-opelidres  34456  difunieq  34658  voliunnfl  34951  dalem20  36844  elpaddn0  36951  cdleme25a  37504  cdleme29ex  37525  cdlemefr29exN  37553  dibglbN  38317  dihlsscpre  38385  lcfl7N  38652  mapdh9a  38940  mapdh9aOLDN  38941  hdmap11lem2  38993  rtprmirr  39214  ax6e2eq  40911  eliin2f  41390  itschlc0xyqsol1  44773