Theorem ancrd 551

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  impac  552  equvinva  2031  sbcg  3809  reuan  3842  2reu1  3843  reupick  4276  reusv2lem3  5336  axprlem4  5362  ssrelrn  5833  relssres  5970  funmo  6497  funssres  6525  dffo4  7036  dffo5  7037  dfwe2  7707  ordpwsuc  7745  ordunisuc2  7774  dfom2  7798  nnsuc  7814  nnaordex  8553  wdom2d  9466  iundom2g  10431  fzospliti  13591  rexuz3  15256  qredeq  16568  prmdvdsfz  16616  dirge  18509  lssssr  20887  lpigen  21272  psgnodpm  21525  psdmul  22081  neiptopnei  23047  metustexhalf  24471  dyadmbllem  25527  3cyclfrgrrn2  30267  atexch  32361  ordtconnlem1  33937  bj-ideqg1  37208  bj-imdirval3  37228  isbasisrelowllem1  37399  isbasisrelowllem2  37400  pibt2  37461  phpreu  37654  poimirlem26  37696  sstotbnd3  37826  eqlkr3  39210  dihatexv  41447  dvh3dim2  41557  unitscyglem4  42301  prjspner1  42729  oasubex  43389  naddwordnexlem4  43504  neik0pk1imk0  44150  pm14.123b  44529  ordpss  44553  climreeq  45723  uspgrlimlem1  48098  itscnhlc0xyqsol  48876