Theorem ancrd 560

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  impac  561  equvinva  2057  sbcg  3825  reuan  3858  2reu1  3859  reupick  4290  reusv2lem3  5372  axprlem4  5398  ssrelrn  5885  relssres  6022  ordpss  6390  funmo  6553  funssres  6581  dffo4  7099  dffo5  7100  dfwe2  7772  ordpwsuc  7810  ordunisuc2  7839  dfom2  7863  nnsuc  7879  nnaordex  8623  wdom2d  9541  iundom2g  10523  fzospliti  13719  rexuz3  15399  qredeq  16714  prmdvdsfz  16763  dirge  18658  lssssr  21052  lpigen  21471  psgnodpm  21706  psdmul  22297  neiptopnei  23257  metustexhalf  24681  dyadmbllem  25726  3cyclfrgrrn2  30578  atexch  32673  ordtconnlem1  34258  bj-ideqg1  37695  bj-imdirval3  37715  isbasisrelowllem1  37888  isbasisrelowllem2  37889  pibt2  37950  phpreu  38142  poimirlem26  38184  sstotbnd3  38314  eqlkr3  39764  dihatexv  42001  dvh3dim2  42111  unitscyglem4  42854  prjspner1  43249  oasubex  43904  naddwordnexlem4  44019  neik0pk1imk0  44664  pm14.123b  45027  climreeq  46220  uspgrlimlem1  48641  itscnhlc0xyqsol  49429