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  3823  reuan  3856  2reu1  3857  reupick  4288  reusv2lem3  5350  axprlem4  5376  ssrelrn  5848  relssres  5982  funmo  6516  funssres  6544  dffo4  7057  dffo5  7058  dfwe2  7730  ordpwsuc  7770  ordunisuc2  7800  dfom2  7824  nnsuc  7840  nnaordex  8579  wdom2d  9509  iundom2g  10469  fzospliti  13628  rexuz3  15291  qredeq  16603  prmdvdsfz  16651  dirge  18544  lssssr  20892  lpigen  21277  psgnodpm  21530  psdmul  22086  neiptopnei  23052  metustexhalf  24477  dyadmbllem  25533  3cyclfrgrrn2  30266  atexch  32360  ordtconnlem1  33907  bj-ideqg1  37145  bj-imdirval3  37165  isbasisrelowllem1  37336  isbasisrelowllem2  37337  pibt2  37398  phpreu  37591  poimirlem26  37633  sstotbnd3  37763  eqlkr3  39087  dihatexv  41325  dvh3dim2  41435  unitscyglem4  42179  prjspner1  42607  oasubex  43268  naddwordnexlem4  43383  neik0pk1imk0  44029  pm14.123b  44408  ordpss  44433  climreeq  45604  uspgrlimlem1  47980  itscnhlc0xyqsol  48747