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

This theorem is referenced by:  impac  552  equvinva  2034  sbcg  3791  reuan  3825  2reu1  3826  reupick  4249  reusv2lem3  5318  ssrelrn  5792  relssres  5921  funmo  6434  funssres  6462  dffo4  6961  dffo5  6962  dfwe2  7602  ordpwsuc  7637  ordunisuc2  7666  dfom2  7689  nnsuc  7705  nnaordex  8431  wdom2d  9269  iundom2g  10227  fzospliti  13347  rexuz3  14988  qredeq  16290  prmdvdsfz  16338  dirge  18236  lssssr  20130  lpigen  20440  psgnodpm  20705  neiptopnei  22191  metustexhalf  23618  dyadmbllem  24668  3cyclfrgrrn2  28552  atexch  30644  ordtconnlem1  31776  bj-ideqg1  35262  bj-imdirval3  35282  isbasisrelowllem1  35453  isbasisrelowllem2  35454  pibt2  35515  phpreu  35688  poimirlem26  35730  sstotbnd3  35861  eqlkr3  37042  dihatexv  39279  dvh3dim2  39389  prjspner1  40384  neik0pk1imk0  41546  pm14.123b  41933  ordpss  41958  climreeq  43044  itscnhlc0xyqsol  45999