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  3856  reuan  3890  2reu1  3891  reupick  4318  reusv2lem3  5398  ssrelrn  5894  relssres  6022  funmo  6563  funmoOLD  6564  funssres  6592  dffo4  7104  dffo5  7105  dfwe2  7760  ordpwsuc  7802  ordunisuc2  7832  dfom2  7856  nnsuc  7872  nnaordex  8637  wdom2d  9574  iundom2g  10534  fzospliti  13663  rexuz3  15294  qredeq  16593  prmdvdsfz  16641  dirge  18555  lssssr  20563  lpigen  20893  psgnodpm  21140  neiptopnei  22635  metustexhalf  24064  dyadmbllem  25115  3cyclfrgrrn2  29537  atexch  31629  ordtconnlem1  32899  bj-ideqg1  36040  bj-imdirval3  36060  isbasisrelowllem1  36231  isbasisrelowllem2  36232  pibt2  36293  phpreu  36467  poimirlem26  36509  sstotbnd3  36639  eqlkr3  37966  dihatexv  40204  dvh3dim2  40314  prjspner1  41369  oasubex  42026  naddwordnexlem4  42142  neik0pk1imk0  42788  pm14.123b  43175  ordpss  43200  climreeq  44319  itscnhlc0xyqsol  47441