Theorem ancrd 552

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  impac  553  equvinva  2033  sbcg  3795  reuan  3829  2reu1  3830  reupick  4252  reusv2lem3  5323  ssrelrn  5803  relssres  5932  funmo  6450  funssres  6478  dffo4  6979  dffo5  6980  dfwe2  7624  ordpwsuc  7662  ordunisuc2  7691  dfom2  7714  nnsuc  7730  nnaordex  8469  wdom2d  9339  iundom2g  10296  fzospliti  13419  rexuz3  15060  qredeq  16362  prmdvdsfz  16410  dirge  18321  lssssr  20215  lpigen  20527  psgnodpm  20793  neiptopnei  22283  metustexhalf  23712  dyadmbllem  24763  3cyclfrgrrn2  28651  atexch  30743  ordtconnlem1  31874  bj-ideqg1  35335  bj-imdirval3  35355  isbasisrelowllem1  35526  isbasisrelowllem2  35527  pibt2  35588  phpreu  35761  poimirlem26  35803  sstotbnd3  35934  eqlkr3  37115  dihatexv  39352  dvh3dim2  39462  prjspner1  40463  neik0pk1imk0  41657  pm14.123b  42044  ordpss  42069  climreeq  43154  itscnhlc0xyqsol  46111