Theorem ancld 550

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  dfmoeu  2535  mopick2  2637  2eu6  2657  cgsexg  3485  cgsex2g  3486  cgsex4g  3487  cgsex4gOLD  3488  reximdva0  4307  difsn  4754  preq12b  4806  elinxp  5978  ssrnres  6136  ordtr2  6362  elunirn  7197  fnoprabg  7481  tz7.49  8376  omord  8495  ficard  10475  fpwwe2lem11  10552  1idpr  10940  xrsupsslem  13222  xrinfmsslem  13223  fzospliti  13607  sqrt2irr  16174  algcvga  16506  prmind2  16612  infpn2  16841  grpinveu  18904  1stcrest  23397  fgss2  23818  fgcl  23822  filufint  23864  metrest  24468  reconnlem2  24772  plydivex  26261  rtprmirr  26726  ftalem3  27041  chtub  27179  lgsqrmodndvds  27320  2sqlem10  27395  dchrisum0flb  27477  pntpbnd1  27553  nolesgn2o  27639  nosupbnd1lem4  27679  noinfbnd1lem4  27694  noetalem1  27709  clwwlkn1loopb  30118  2pthfrgrrn2  30358  grpoidinvlem3  30581  grpoinveu  30594  elim2ifim  32620  iocinif  32861  qsxpid  33443  tpr2rico  34069  bnj168  34886  ellcsrspsn  35835  dfon2lem8  35982  nn0prpwlem  36516  bj-opelidres  37366  difunieq  37579  voliunnfl  37865  dalem20  39953  elpaddn0  40060  cdleme25a  40613  cdleme29ex  40634  cdlemefr29exN  40662  dibglbN  41426  dihlsscpre  41494  lcfl7N  41761  mapdh9a  42049  mapdh9aOLDN  42050  hdmap11lem2  42102  eu6w  42919  sqrtcval  43882  ax6e2eq  44798  eliin2f  45348  clnbgr3stgrgrlic  48266  itschlc0xyqsol1  49012  mpbiran3d  49042