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  3482  cgsex2g  3483  cgsex4g  3484  cgsex4gOLD  3485  reximdva0  4304  difsn  4751  preq12b  4803  elinxp  5975  ssrnres  6133  ordtr2  6359  elunirn  7194  fnoprabg  7478  tz7.49  8373  omord  8492  ficard  10467  fpwwe2lem11  10543  1idpr  10931  xrsupsslem  13213  xrinfmsslem  13214  fzospliti  13598  sqrt2irr  16165  algcvga  16497  prmind2  16603  infpn2  16832  grpinveu  18895  1stcrest  23388  fgss2  23809  fgcl  23813  filufint  23855  metrest  24459  reconnlem2  24763  plydivex  26252  rtprmirr  26717  ftalem3  27032  chtub  27170  lgsqrmodndvds  27311  2sqlem10  27386  dchrisum0flb  27468  pntpbnd1  27544  nolesgn2o  27630  nosupbnd1lem4  27670  noinfbnd1lem4  27685  noetalem1  27700  clwwlkn1loopb  30044  2pthfrgrrn2  30284  grpoidinvlem3  30507  grpoinveu  30520  elim2ifim  32546  iocinif  32789  qsxpid  33371  tpr2rico  33997  bnj168  34814  ellcsrspsn  35757  dfon2lem8  35904  nn0prpwlem  36438  bj-opelidres  37278  difunieq  37491  voliunnfl  37777  dalem20  39865  elpaddn0  39972  cdleme25a  40525  cdleme29ex  40546  cdlemefr29exN  40574  dibglbN  41338  dihlsscpre  41406  lcfl7N  41673  mapdh9a  41961  mapdh9aOLDN  41962  hdmap11lem2  42014  eu6w  42834  sqrtcval  43798  ax6e2eq  44714  eliin2f  45264  clnbgr3stgrgrlic  48182  itschlc0xyqsol1  48928  mpbiran3d  48958