Theorem ancrd 551

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  impac  552  equvinva  2029  sbcg  3883  reuan  3918  2reu1  3919  reupick  4348  reusv2lem3  5418  ssrelrn  5919  relssres  6051  funmo  6593  funmoOLD  6594  funssres  6622  dffo4  7137  dffo5  7138  dfwe2  7809  ordpwsuc  7851  ordunisuc2  7881  dfom2  7905  nnsuc  7921  nnaordex  8694  wdom2d  9649  iundom2g  10609  fzospliti  13748  rexuz3  15397  qredeq  16704  prmdvdsfz  16752  dirge  18673  lssssr  20975  lpigen  21368  psgnodpm  21629  psdmul  22193  neiptopnei  23161  metustexhalf  24590  dyadmbllem  25653  3cyclfrgrrn2  30319  atexch  32413  ordtconnlem1  33870  bj-ideqg1  37130  bj-imdirval3  37150  isbasisrelowllem1  37321  isbasisrelowllem2  37322  pibt2  37383  phpreu  37564  poimirlem26  37606  sstotbnd3  37736  eqlkr3  39057  dihatexv  41295  dvh3dim2  41405  unitscyglem4  42155  prjspner1  42581  oasubex  43248  naddwordnexlem4  43363  neik0pk1imk0  44009  pm14.123b  44395  ordpss  44420  climreeq  45534  uspgrlimlem1  47812  itscnhlc0xyqsol  48499