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  5362  axprlem4  5388  ssrelrn  5876  relssres  6011  ordpss  6391  funmo  6554  funssres  6584  dffo4  7103  dffo5  7104  dfwe2  7788  ordpwsuc  7826  ordunisuc2  7855  dfom2  7879  nnsuc  7895  nnaordex  8647  wdom2d  9574  iundom2g  10624  fzospliti  13826  rexuz3  15516  qredeq  16832  prmdvdsfz  16881  dirge  18777  lssssr  21229  lpigen  21659  psgnodpm  21894  psdmul  22487  neiptopnei  23450  metustexhalf  24875  dyadmbllem  25920  3cyclfrgrrn2  30888  atexch  32983  ordtconnlem1  34556  bj-ideqg1  38085  bj-imdirval3  38105  isbasisrelowllem1  38278  isbasisrelowllem2  38279  pibt2  38340  phpreu  38527  poimirlem26  38564  sstotbnd3  38710  eqlkr3  40158  dihatexv  42395  dvh3dim2  42505  unitscyglem4  43248  oasubex  44287  naddwordnexlem4  44402  neik0pk1imk0  45046  pm14.123b  45409  climreeq  46624  uspgrlimlem1  49085  itscnhlc0xyqsol  49876