Theorem ancld 574

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 554	1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  equvinv  1946  equvinivOLD  1948  mo2v  2465  mopick2  2528  2eu6  2546  cgsexg  3211  cgsex2g  3212  cgsex4g  3213  reximdva0  3891  difsn  4269  preq12b  4322  elres  5355  relssres  5357  ordtr2  5685  elunirn  6413  fnoprabg  6659  tz7.49  7427  omord  7535  ficard  9266  fpwwe2lem12  9342  1idpr  9730  xrsupsslem  12009  xrinfmsslem  12010  fzospliti  12369  sqrt2irr  14817  algcvga  15130  prmind2  15236  infpn2  15455  grpinveu  17279  1stcrest  21066  fgss2  21488  fgcl  21492  filufint  21534  metrest  22139  reconnlem2  22438  plydivex  23856  ftalem3  24601  chtub  24737  lgsqrmodndvds  24878  2sqlem10  24953  dchrisum0flb  24999  pntpbnd1  25075  2pthfrgrarn2  26537  grpoidinvlem3  26744  grpoinveu  26757  elim2ifim  28748  iocinif  28933  tpr2rico  29286  bnj168  30052  dfon2lem8  30939  dftrpred3g  30977  nofulllem5  31105  nn0prpwlem  31487  voliunnfl  32623  dalem20  33997  elpaddn0  34104  cdleme25a  34659  cdleme29ex  34680  cdlemefr29exN  34708  dibglbN  35473  dihlsscpre  35541  lcfl7N  35808  mapdh9a  36097  mapdh9aOLDN  36098  hdmap11lem2  36152  ax6e2eq  37794  eliin2f  38316  2pthfrgrrn2  41453