Theorem ancrd 576

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  impac  650  equviniva  2004  reupick  3944  prel12  4414  reusv2lem3  4901  ssrelrn  5347  ssrnres  5607  funmo  5942  funssres  5968  dffo4  6415  dffo5  6416  dfwe2  7023  ordpwsuc  7057  ordunisuc2  7086  dfom2  7109  nnsuc  7124  nnaordex  7763  wdom2d  8526  iundom2g  9400  fzospliti  12539  rexuz3  14132  qredeq  15418  prmdvdsfz  15464  dirge  17284  lssssr  19001  lpigen  19304  psgnodpm  19982  neiptopnei  20984  metustexhalf  22408  dyadmbllem  23413  3cyclfrgrrn2  27267  atexch  29368  ordtconnlem1  30098  isbasisrelowllem1  33333  isbasisrelowllem2  33334  phpreu  33523  poimirlem26  33565  sstotbnd3  33705  eqlkr3  34706  dihatexv  36944  dvh3dim2  37054  neik0pk1imk0  38662  pm14.123b  38944  ordpss  38972  climreeq  40163  reuan  41501  2reu1  41507