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  2531  mopick2  2632  2eu6  2652  cgsexg  3481  cgsex2g  3482  cgsex4g  3483  cgsex4gOLD  3484  reximdva0  4300  difsn  4745  preq12b  4797  elinxp  5963  ssrnres  6120  ordtr2  6346  elunirn  7180  fnoprabg  7464  tz7.49  8359  omord  8478  ficard  10451  fpwwe2lem11  10527  1idpr  10915  xrsupsslem  13201  xrinfmsslem  13202  fzospliti  13586  sqrt2irr  16153  algcvga  16485  prmind2  16591  infpn2  16820  grpinveu  18882  1stcrest  23363  fgss2  23784  fgcl  23788  filufint  23830  metrest  24434  reconnlem2  24738  plydivex  26227  rtprmirr  26692  ftalem3  27007  chtub  27145  lgsqrmodndvds  27286  2sqlem10  27361  dchrisum0flb  27443  pntpbnd1  27519  nolesgn2o  27605  nosupbnd1lem4  27645  noinfbnd1lem4  27660  noetalem1  27675  clwwlkn1loopb  30015  2pthfrgrrn2  30255  grpoidinvlem3  30478  grpoinveu  30491  elim2ifim  32517  iocinif  32756  qsxpid  33319  tpr2rico  33917  bnj168  34734  ellcsrspsn  35677  dfon2lem8  35824  nn0prpwlem  36356  bj-opelidres  37195  difunieq  37408  voliunnfl  37704  dalem20  39732  elpaddn0  39839  cdleme25a  40392  cdleme29ex  40413  cdlemefr29exN  40441  dibglbN  41205  dihlsscpre  41273  lcfl7N  41540  mapdh9a  41828  mapdh9aOLDN  41829  hdmap11lem2  41881  eu6w  42709  sqrtcval  43674  ax6e2eq  44590  eliin2f  45141  clnbgr3stgrgrlic  48051  itschlc0xyqsol1  48798  mpbiran3d  48828