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  2063  sbcg  3811  reuan  3844  2reu1  3845  reupick  4275  reusv2lem3  5365  axprlem4  5391  ssrelrn  5878  relssres  6015  ordpss  6386  funmo  6549  funssres  6577  dffo4  7096  dffo5  7097  dfwe2  7773  ordpwsuc  7811  ordunisuc2  7840  dfom2  7864  nnsuc  7880  nnaordex  8626  wdom2d  9552  iundom2g  10548  fzospliti  13747  rexuz3  15436  qredeq  16747  prmdvdsfz  16796  dirge  18691  lssssr  21138  lpigen  21566  psgnodpm  21801  psdmul  22394  neiptopnei  23357  metustexhalf  24782  dyadmbllem  25827  3cyclfrgrrn2  30767  atexch  32862  ordtconnlem1  34434  bj-ideqg1  37916  bj-imdirval3  37936  isbasisrelowllem1  38109  isbasisrelowllem2  38110  pibt2  38171  phpreu  38358  poimirlem26  38395  sstotbnd3  38526  eqlkr3  39974  dihatexv  42211  dvh3dim2  42321  unitscyglem4  43064  prjspner1  43472  oasubex  44127  naddwordnexlem4  44242  neik0pk1imk0  44887  pm14.123b  45250  climreeq  46443  uspgrlimlem1  48904  itscnhlc0xyqsol  49695