Theorem ancrd 559

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  impac  560  equvinva  2050  sbcg  3816  reuan  3849  2reu1  3850  reupick  4281  reusv2lem3  5357  axprlem4  5383  ssrelrn  5870  relssres  6008  funmo  6537  funssres  6565  dffo4  7084  dffo5  7085  dfwe2  7757  ordpwsuc  7795  ordunisuc2  7824  dfom2  7848  nnsuc  7864  nnaordex  8608  wdom2d  9528  iundom2g  10497  fzospliti  13697  rexuz3  15376  qredeq  16691  prmdvdsfz  16740  dirge  18635  lssssr  21021  lpigen  21405  psgnodpm  21640  psdmul  22231  neiptopnei  23192  metustexhalf  24616  dyadmbllem  25661  3cyclfrgrrn2  30489  atexch  32584  ordtconnlem1  34221  bj-ideqg1  37656  bj-imdirval3  37676  isbasisrelowllem1  37849  isbasisrelowllem2  37850  pibt2  37911  phpreu  38103  poimirlem26  38145  sstotbnd3  38275  eqlkr3  39725  dihatexv  41962  dvh3dim2  42072  unitscyglem4  42815  prjspner1  43208  oasubex  43863  naddwordnexlem4  43978  neik0pk1imk0  44623  pm14.123b  45002  ordpss  45026  climreeq  46189  uspgrlimlem1  48610  itscnhlc0xyqsol  49387