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  2030  sbcg  3823  reuan  3856  2reu1  3857  reupick  4288  reusv2lem3  5350  axprlem4  5376  ssrelrn  5848  relssres  5982  funmo  6516  funssres  6544  dffo4  7057  dffo5  7058  dfwe2  7730  ordpwsuc  7770  ordunisuc2  7800  dfom2  7824  nnsuc  7840  nnaordex  8579  wdom2d  9509  iundom2g  10469  fzospliti  13628  rexuz3  15291  qredeq  16603  prmdvdsfz  16651  dirge  18538  lssssr  20836  lpigen  21221  psgnodpm  21473  psdmul  22029  neiptopnei  22995  metustexhalf  24420  dyadmbllem  25476  3cyclfrgrrn2  30189  atexch  32283  ordtconnlem1  33887  bj-ideqg1  37125  bj-imdirval3  37145  isbasisrelowllem1  37316  isbasisrelowllem2  37317  pibt2  37378  phpreu  37571  poimirlem26  37613  sstotbnd3  37743  eqlkr3  39067  dihatexv  41305  dvh3dim2  41415  unitscyglem4  42159  prjspner1  42587  oasubex  43248  naddwordnexlem4  43363  neik0pk1imk0  44009  pm14.123b  44388  ordpss  44413  climreeq  45584  uspgrlimlem1  47960  itscnhlc0xyqsol  48727