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  2032  sbcg  3802  reuan  3835  2reu1  3836  reupick  4270  reusv2lem3  5338  axprlem4  5364  ssrelrn  5844  relssres  5982  funmo  6509  funssres  6537  dffo4  7050  dffo5  7051  dfwe2  7722  ordpwsuc  7760  ordunisuc2  7789  dfom2  7813  nnsuc  7829  nnaordex  8568  wdom2d  9489  iundom2g  10456  fzospliti  13640  rexuz3  15305  qredeq  16620  prmdvdsfz  16669  dirge  18563  lssssr  20943  lpigen  21328  psgnodpm  21581  psdmul  22145  neiptopnei  23110  metustexhalf  24534  dyadmbllem  25579  3cyclfrgrrn2  30375  atexch  32470  ordtconnlem1  34087  bj-ideqg1  37497  bj-imdirval3  37517  isbasisrelowllem1  37688  isbasisrelowllem2  37689  pibt2  37750  phpreu  37942  poimirlem26  37984  sstotbnd3  38114  eqlkr3  39564  dihatexv  41801  dvh3dim2  41911  unitscyglem4  42654  prjspner1  43076  oasubex  43735  naddwordnexlem4  43850  neik0pk1imk0  44495  pm14.123b  44874  ordpss  44898  climreeq  46064  uspgrlimlem1  48479  itscnhlc0xyqsol  49256