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  2030  sbcg  3815  reuan  3848  2reu1  3849  reupick  4280  reusv2lem3  5339  axprlem4  5365  ssrelrn  5837  relssres  5973  funmo  6498  funssres  6526  dffo4  7037  dffo5  7038  dfwe2  7710  ordpwsuc  7748  ordunisuc2  7777  dfom2  7801  nnsuc  7817  nnaordex  8556  wdom2d  9472  iundom2g  10434  fzospliti  13594  rexuz3  15256  qredeq  16568  prmdvdsfz  16616  dirge  18509  lssssr  20857  lpigen  21242  psgnodpm  21495  psdmul  22051  neiptopnei  23017  metustexhalf  24442  dyadmbllem  25498  3cyclfrgrrn2  30231  atexch  32325  ordtconnlem1  33891  bj-ideqg1  37142  bj-imdirval3  37162  isbasisrelowllem1  37333  isbasisrelowllem2  37334  pibt2  37395  phpreu  37588  poimirlem26  37630  sstotbnd3  37760  eqlkr3  39084  dihatexv  41321  dvh3dim2  41431  unitscyglem4  42175  prjspner1  42603  oasubex  43263  naddwordnexlem4  43378  neik0pk1imk0  44024  pm14.123b  44403  ordpss  44428  climreeq  45598  uspgrlimlem1  47976  itscnhlc0xyqsol  48754