Theorem ancrd 561

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 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜓))
3	1, 2	jcad 522	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜓)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  impac  562  equvinva  2062  sbcg  3810  reuan  3844  2reu1  3845  reupick  4273  reusv2lem3  5362  axprlem4  5388  ssrelrn  5877  relssres  6013  ordpss  6394  funmo  6559  funssres  6589  dffo4  7108  dffo5  7109  dfwe2  7792  ordpwsuc  7830  ordunisuc2  7859  dfom2  7883  nnsuc  7899  nnaordex  8655  wdom2d  9581  iundom2g  10631  fzospliti  13833  rexuz3  15525  qredeq  16841  prmdvdsfz  16890  dirge  18786  lssssr  21238  lpigen  21668  psgnodpm  21903  psdmul  22496  neiptopnei  23459  metustexhalf  24884  dyadmbllem  25929  3cyclfrgrrn2  30897  atexch  32992  ordtconnlem1  34606  ptpconn  36116  bj-ideqg1  38222  bj-imdirval3  38242  isbasisrelowllem1  38415  isbasisrelowllem2  38416  pibt2  38477  phpreu  38664  poimirlem26  38701  sstotbnd3  38847  eqlkr3  40295  dihatexv  42532  dvh3dim2  42642  unitscyglem4  43385  oasubex  44425  naddwordnexlem4  44540  neik0pk1imk0  45184  pm14.123b  45546  climreeq  46761  uspgrlimlem1  49222  itscnhlc0xyqsol  50013