Theorem ancrd 551

Description: Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)

Hypothesis

Ref	Expression
ancrd.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
ancrd	⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜓)))

Proof of Theorem ancrd

Step	Hyp	Ref	Expression
1		ancrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		idd 24	. 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:  impac  552  equvinva  2031  sbcg  3811  reuan  3844  2reu1  3845  reupick  4280  reusv2lem3  5342  axprlem4  5368  ssrelrn  5841  relssres  5978  funmo  6505  funssres  6533  dffo4  7045  dffo5  7046  dfwe2  7716  ordpwsuc  7754  ordunisuc2  7783  dfom2  7807  nnsuc  7823  nnaordex  8562  wdom2d  9476  iundom2g  10441  fzospliti  13601  rexuz3  15266  qredeq  16578  prmdvdsfz  16626  dirge  18519  lssssr  20897  lpigen  21282  psgnodpm  21535  psdmul  22091  neiptopnei  23057  metustexhalf  24481  dyadmbllem  25537  3cyclfrgrrn2  30278  atexch  32372  ordtconnlem1  33948  bj-ideqg1  37219  bj-imdirval3  37239  isbasisrelowllem1  37410  isbasisrelowllem2  37411  pibt2  37472  phpreu  37654  poimirlem26  37696  sstotbnd3  37826  eqlkr3  39210  dihatexv  41447  dvh3dim2  41557  unitscyglem4  42301  prjspner1  42734  oasubex  43393  naddwordnexlem4  43508  neik0pk1imk0  44154  pm14.123b  44533  ordpss  44557  climreeq  45727  uspgrlimlem1  48102  itscnhlc0xyqsol  48880