Theorem ancrd 576

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  impac  650  equviniva  1957  reupick  3887  prel12  4351  reusv2lem3  4831  ssrelrn  5275  ssrnres  5531  funmo  5863  funssres  5888  dffo4  6331  dffo5  6332  dfwe2  6928  ordpwsuc  6962  ordunisuc2  6991  dfom2  7014  nnsuc  7029  nnaordex  7663  wdom2d  8429  iundom2g  9306  fzospliti  12441  rexuz3  14022  qredeq  15295  prmdvdsfz  15341  dirge  17158  lssssr  18872  lpigen  19175  psgnodpm  19853  neiptopnei  20846  metustexhalf  22271  dyadmbllem  23273  3cyclfrgrrn2  27015  atexch  29086  ordtconnlem1  29749  isbasisrelowllem1  32832  isbasisrelowllem2  32833  phpreu  33022  poimirlem26  33064  sstotbnd3  33204  eqlkr3  33865  dihatexv  36104  dvh3dim2  36214  neik0pk1imk0  37824  pm14.123b  38106  ordpss  38134  climreeq  39246  reuan  40481  2reu1  40487