Theorem ancrd 561

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 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜓))
3	1, 2	jcad 522	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜓)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  impac  562  equvinva  2063  sbcg  3818  reuan  3851  2reu1  3852  reupick  4282  reusv2lem3  5373  axprlem4  5399  ssrelrn  5886  relssres  6023  ordpss  6393  funmo  6556  funssres  6584  dffo4  7102  dffo5  7103  dfwe2  7779  ordpwsuc  7817  ordunisuc2  7846  dfom2  7870  nnsuc  7886  nnaordex  8630  wdom2d  9549  iundom2g  10541  fzospliti  13739  rexuz3  15426  qredeq  16739  prmdvdsfz  16788  dirge  18683  lssssr  21127  lpigen  21555  psgnodpm  21790  psdmul  22381  neiptopnei  23341  metustexhalf  24766  dyadmbllem  25811  3cyclfrgrrn2  30711  atexch  32806  ordtconnlem1  34380  bj-ideqg1  37867  bj-imdirval3  37887  isbasisrelowllem1  38060  isbasisrelowllem2  38061  pibt2  38122  phpreu  38314  poimirlem26  38356  sstotbnd3  38487  eqlkr3  39935  dihatexv  42172  dvh3dim2  42282  unitscyglem4  43025  prjspner1  43418  oasubex  44073  naddwordnexlem4  44188  neik0pk1imk0  44833  pm14.123b  45196  climreeq  46389  uspgrlimlem1  48813  itscnhlc0xyqsol  49604