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  2065  sbcg  3814  reuan  3848  2reu1  3849  reupick  4277  reusv2lem3  5369  axprlem4  5395  ssrelrn  5888  relssres  6029  ordpss  6417  funmo  6582  funssres  6612  dffo4  7135  dffo5  7136  dfwe2  7820  ordpwsuc  7860  ordunisuc2  7889  dfom2  7913  nnsuc  7929  nnaordex  8685  wdom2d  9611  iundom2g  10663  fzospliti  13866  rexuz3  15560  qredeq  16876  prmdvdsfz  16925  dirge  18827  lssssr  21280  lpigen  21710  psgnodpm  21949  psdmul  22542  neiptopnei  23505  metustexhalf  24930  dyadmbllem  25975  3cyclfrgrrn2  30945  atexch  33040  ordtconnlem1  34667  ptpconn  36206  bj-ideqg1  38353  bj-imdirval3  38373  isbasisrelowllem1  38546  isbasisrelowllem2  38547  pibt2  38608  phpreu  38795  poimirlem26  38832  sstotbnd3  38976  eqlkr3  40424  dihatexv  42661  dvh3dim2  42771  unitscyglem4  43514  oasubex  44549  naddwordnexlem4  44664  neik0pk1imk0  45308  pm14.123b  45670  climreeq  46898  uspgrlimlem1  49359  itscnhlc0xyqsol  50208