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  3811  reuan  3844  2reu1  3845  reupick  4275  reusv2lem3  5365  axprlem4  5391  ssrelrn  5878  relssres  6015  ordpss  6386  funmo  6549  funssres  6578  dffo4  7097  dffo5  7098  dfwe2  7774  ordpwsuc  7812  ordunisuc2  7841  dfom2  7865  nnsuc  7881  nnaordex  8627  wdom2d  9553  iundom2g  10549  fzospliti  13748  rexuz3  15437  qredeq  16748  prmdvdsfz  16797  dirge  18692  lssssr  21139  lpigen  21567  psgnodpm  21802  psdmul  22395  neiptopnei  23358  metustexhalf  24783  dyadmbllem  25828  3cyclfrgrrn2  30768  atexch  32863  ordtconnlem1  34435  bj-ideqg1  37917  bj-imdirval3  37937  isbasisrelowllem1  38110  isbasisrelowllem2  38111  pibt2  38172  phpreu  38359  poimirlem26  38396  sstotbnd3  38527  eqlkr3  39975  dihatexv  42212  dvh3dim2  42322  unitscyglem4  43065  prjspner1  43473  oasubex  44128  naddwordnexlem4  44243  neik0pk1imk0  44888  pm14.123b  45251  climreeq  46444  uspgrlimlem1  48905  itscnhlc0xyqsol  49696