Theorem ancld 560

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  dfmoeu  2561  mopick2  2663  2eu6  2682  cgsexg  3495  cgsex2g  3496  cgsex4g  3497  reximdva0  4303  difsn  4761  preq12b  4810  elrelb  5775  elinxp  6008  ssrnres  6170  ordtr2  6407  elunirn  7253  fnoprabg  7541  tz7.49  8448  omord  8569  ficard  10642  fpwwe2lem11  10719  1idpr  11107  xrsupsslem  13430  xrinfmsslem  13431  fzospliti  13819  sqrt2irr  16410  algcvga  16747  prmind2  16853  infpn2  17084  grpinveu  19178  qsxpid  19380  1stcrest  23764  fgss2  24186  fgcl  24190  filufint  24232  metrest  24836  reconnlem2  25140  plydivex  26611  rtprmirr  27081  ftalem3  27395  chtub  27532  lgsqrmodndvds  27673  2sqlem10  27748  dchrisum0flb  27830  pntpbnd1  27906  nolesgn2o  28021  nosupbnd1lem4  28061  noinfbnd1lem4  28076  noetalem1  28091  clwwlkn1loopb  30627  2pthfrgrrn2  30877  grpoidinvlem3  31101  grpoinveu  31114  elim2ifim  33134  iocinif  33366  tpr2rico  34537  bnj168  35354  karddom  35812  kardsdom  35813  ellcsrspsn  36385  dfon2lem8  36532  nn0prpwlem  37090  cgsex2gd  38038  bj-opelidres  38062  difunieq  38277  voliunnfl  38562  dalem20  40730  elpaddn0  40837  cdleme25a  41390  cdleme29ex  41411  cdlemefr29exN  41439  dibglbN  42203  dihlsscpre  42271  lcfl7N  42538  mapdh9a  42826  mapdh9aOLDN  42827  hdmap11lem2  42879  eu6w  43667  sqrtcval  44626  ax6e2eq  45525  eliin2f  46088  clnbgr3stgrgrlic  49087  itschlc0xyqsol1  49847  mpbiran3d  49876