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  2533  mopick2  2634  2eu6  2654  cgsexg  3523  cgsex2g  3524  cgsex4g  3525  cgsex4gOLD  3526  reximdva0  4360  difsn  4802  preq12b  4854  elinxp  6038  ssrnres  6199  ordtr2  6429  elunirn  7270  fnoprabg  7555  tz7.49  8483  omord  8604  ficard  10602  fpwwe2lem11  10678  1idpr  11066  xrsupsslem  13345  xrinfmsslem  13346  fzospliti  13727  sqrt2irr  16281  algcvga  16612  prmind2  16718  infpn2  16946  grpinveu  19004  1stcrest  23476  fgss2  23897  fgcl  23901  filufint  23943  metrest  24552  reconnlem2  24862  plydivex  26353  rtprmirr  26817  ftalem3  27132  chtub  27270  lgsqrmodndvds  27411  2sqlem10  27486  dchrisum0flb  27568  pntpbnd1  27644  nolesgn2o  27730  nosupbnd1lem4  27770  noinfbnd1lem4  27785  noetalem1  27800  clwwlkn1loopb  30071  2pthfrgrrn2  30311  grpoidinvlem3  30534  grpoinveu  30547  elim2ifim  32565  iocinif  32789  qsxpid  33369  tpr2rico  33872  bnj168  34722  ellcsrspsn  35625  dfon2lem8  35771  nn0prpwlem  36304  bj-opelidres  37143  difunieq  37356  voliunnfl  37650  dalem20  39675  elpaddn0  39782  cdleme25a  40335  cdleme29ex  40356  cdlemefr29exN  40384  dibglbN  41148  dihlsscpre  41216  lcfl7N  41483  mapdh9a  41771  mapdh9aOLDN  41772  hdmap11lem2  41824  eu6w  42662  sqrtcval  43630  ax6e2eq  44554  eliin2f  45043  clnbgr3stgrgrlic  47914  itschlc0xyqsol1  48615  mpbiran3d  48645