Theorem ancrd 553

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  impac  554  equvinva  2033  sbcg  3813  reuan  3847  2reu1  3848  reupick  4273  reusv2lem3  5350  ssrelrn  5843  relssres  5971  funmo  6508  funmoOLD  6509  funssres  6537  dffo4  7044  dffo5  7045  dfwe2  7695  ordpwsuc  7737  ordunisuc2  7767  dfom2  7791  nnsuc  7807  nnaordex  8549  wdom2d  9446  iundom2g  10406  fzospliti  13529  rexuz3  15164  qredeq  16464  prmdvdsfz  16512  dirge  18423  lssssr  20325  lpigen  20637  psgnodpm  20903  neiptopnei  22393  metustexhalf  23822  dyadmbllem  24873  3cyclfrgrrn2  29005  atexch  31097  ordtconnlem1  32236  bj-ideqg1  35491  bj-imdirval3  35511  isbasisrelowllem1  35682  isbasisrelowllem2  35683  pibt2  35744  phpreu  35917  poimirlem26  35959  sstotbnd3  36090  eqlkr3  37419  dihatexv  39657  dvh3dim2  39767  prjspner1  40776  neik0pk1imk0  42030  pm14.123b  42417  ordpss  42442  climreeq  43542  itscnhlc0xyqsol  46529