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  2636  2eu6  2656  cgsexg  3505  cgsex2g  3506  cgsex4g  3507  cgsex4gOLD  3508  reximdva0  4330  difsn  4774  preq12b  4826  elinxp  6006  ssrnres  6167  ordtr2  6397  elunirn  7243  fnoprabg  7530  tz7.49  8459  omord  8580  ficard  10579  fpwwe2lem11  10655  1idpr  11043  xrsupsslem  13323  xrinfmsslem  13324  fzospliti  13708  sqrt2irr  16267  algcvga  16598  prmind2  16704  infpn2  16933  grpinveu  18957  1stcrest  23391  fgss2  23812  fgcl  23816  filufint  23858  metrest  24463  reconnlem2  24767  plydivex  26257  rtprmirr  26722  ftalem3  27037  chtub  27175  lgsqrmodndvds  27316  2sqlem10  27391  dchrisum0flb  27473  pntpbnd1  27549  nolesgn2o  27635  nosupbnd1lem4  27675  noinfbnd1lem4  27690  noetalem1  27705  clwwlkn1loopb  30024  2pthfrgrrn2  30264  grpoidinvlem3  30487  grpoinveu  30500  elim2ifim  32526  iocinif  32758  qsxpid  33377  tpr2rico  33943  bnj168  34761  ellcsrspsn  35663  dfon2lem8  35808  nn0prpwlem  36340  bj-opelidres  37179  difunieq  37392  voliunnfl  37688  dalem20  39712  elpaddn0  39819  cdleme25a  40372  cdleme29ex  40393  cdlemefr29exN  40421  dibglbN  41185  dihlsscpre  41253  lcfl7N  41520  mapdh9a  41808  mapdh9aOLDN  41809  hdmap11lem2  41861  eu6w  42699  sqrtcval  43665  ax6e2eq  44582  eliin2f  45128  clnbgr3stgrgrlic  48024  itschlc0xyqsol1  48746  mpbiran3d  48776