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  2031  sbcg  3811  reuan  3844  2reu1  3845  reupick  4279  reusv2lem3  5343  axprlem4  5369  ssrelrn  5841  relssres  5979  funmo  6506  funssres  6534  dffo4  7046  dffo5  7047  dfwe2  7717  ordpwsuc  7755  ordunisuc2  7784  dfom2  7808  nnsuc  7824  nnaordex  8564  wdom2d  9483  iundom2g  10448  fzospliti  13605  rexuz3  15270  qredeq  16582  prmdvdsfz  16630  dirge  18524  lssssr  20903  lpigen  21288  psgnodpm  21541  psdmul  22107  neiptopnei  23074  metustexhalf  24498  dyadmbllem  25554  3cyclfrgrrn2  30311  atexch  32405  ordtconnlem1  34030  bj-ideqg1  37308  bj-imdirval3  37328  isbasisrelowllem1  37499  isbasisrelowllem2  37500  pibt2  37561  phpreu  37744  poimirlem26  37786  sstotbnd3  37916  eqlkr3  39300  dihatexv  41537  dvh3dim2  41647  unitscyglem4  42391  prjspner1  42811  oasubex  43470  naddwordnexlem4  43585  neik0pk1imk0  44230  pm14.123b  44609  ordpss  44633  climreeq  45801  uspgrlimlem1  48176  itscnhlc0xyqsol  48953