Theorem ancrd 553

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  impac  554  equvinva  2034  sbcg  3857  reuan  3891  2reu1  3892  reupick  4319  reusv2lem3  5399  ssrelrn  5895  relssres  6023  funmo  6564  funmoOLD  6565  funssres  6593  dffo4  7105  dffo5  7106  dfwe2  7761  ordpwsuc  7803  ordunisuc2  7833  dfom2  7857  nnsuc  7873  nnaordex  8638  wdom2d  9575  iundom2g  10535  fzospliti  13664  rexuz3  15295  qredeq  16594  prmdvdsfz  16642  dirge  18556  lssssr  20564  lpigen  20894  psgnodpm  21141  neiptopnei  22636  metustexhalf  24065  dyadmbllem  25116  3cyclfrgrrn2  29540  atexch  31634  ordtconnlem1  32904  bj-ideqg1  36045  bj-imdirval3  36065  isbasisrelowllem1  36236  isbasisrelowllem2  36237  pibt2  36298  phpreu  36472  poimirlem26  36514  sstotbnd3  36644  eqlkr3  37971  dihatexv  40209  dvh3dim2  40319  prjspner1  41368  oasubex  42036  naddwordnexlem4  42152  neik0pk1imk0  42798  pm14.123b  43185  ordpss  43210  climreeq  44329  itscnhlc0xyqsol  47451