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  2536  mopick2  2638  2eu6  2658  cgsexg  3475  cgsex2g  3476  cgsex4g  3477  reximdva0  4296  difsn  4742  preq12b  4794  elinxp  5976  ssrnres  6134  ordtr2  6360  elunirn  7197  fnoprabg  7481  tz7.49  8375  omord  8494  ficard  10476  fpwwe2lem11  10553  1idpr  10941  xrsupsslem  13248  xrinfmsslem  13249  fzospliti  13635  sqrt2irr  16205  algcvga  16537  prmind2  16643  infpn2  16873  grpinveu  18939  1stcrest  23427  fgss2  23848  fgcl  23852  filufint  23894  metrest  24498  reconnlem2  24802  plydivex  26276  rtprmirr  26741  ftalem3  27056  chtub  27194  lgsqrmodndvds  27335  2sqlem10  27410  dchrisum0flb  27492  pntpbnd1  27568  nolesgn2o  27654  nosupbnd1lem4  27694  noinfbnd1lem4  27709  noetalem1  27724  clwwlkn1loopb  30133  2pthfrgrrn2  30373  grpoidinvlem3  30597  grpoinveu  30610  elim2ifim  32635  iocinif  32874  qsxpid  33442  tpr2rico  34077  bnj168  34894  ellcsrspsn  35844  dfon2lem8  35991  nn0prpwlem  36525  cgsex2gd  37464  bj-opelidres  37488  difunieq  37701  voliunnfl  37996  dalem20  40150  elpaddn0  40257  cdleme25a  40810  cdleme29ex  40831  cdlemefr29exN  40859  dibglbN  41623  dihlsscpre  41691  lcfl7N  41958  mapdh9a  42246  mapdh9aOLDN  42247  hdmap11lem2  42299  eu6w  43120  sqrtcval  44083  ax6e2eq  44999  eliin2f  45549  clnbgr3stgrgrlic  48493  itschlc0xyqsol1  49239  mpbiran3d  49269