Theorem ancrd 560

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 521	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜓)))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  impac  561  equvinva  2060  sbcg  3816  reuan  3850  2reu1  3851  reupick  4282  reusv2lem3  5371  axprlem4  5397  ssrelrn  5884  relssres  6021  ordpss  6389  funmo  6552  funssres  6580  dffo4  7098  dffo5  7099  dfwe2  7769  ordpwsuc  7807  ordunisuc2  7836  dfom2  7860  nnsuc  7876  nnaordex  8620  wdom2d  9538  iundom2g  10519  fzospliti  13716  rexuz3  15396  qredeq  16710  prmdvdsfz  16759  dirge  18654  lssssr  21075  lpigen  21503  psgnodpm  21738  psdmul  22329  neiptopnei  23289  metustexhalf  24713  dyadmbllem  25758  3cyclfrgrrn2  30638  atexch  32733  ordtconnlem1  34314  bj-ideqg1  37828  bj-imdirval3  37848  isbasisrelowllem1  38021  isbasisrelowllem2  38022  pibt2  38083  phpreu  38275  poimirlem26  38317  sstotbnd3  38447  eqlkr3  39895  dihatexv  42132  dvh3dim2  42242  unitscyglem4  42985  prjspner1  43378  oasubex  44033  naddwordnexlem4  44148  neik0pk1imk0  44793  pm14.123b  45156  climreeq  46349  uspgrlimlem1  48773  itscnhlc0xyqsol  49565