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  3813  reuan  3846  2reu1  3847  reupick  4281  reusv2lem3  5345  axprlem4  5371  ssrelrn  5843  relssres  5981  funmo  6508  funssres  6536  dffo4  7048  dffo5  7049  dfwe2  7719  ordpwsuc  7757  ordunisuc2  7786  dfom2  7810  nnsuc  7826  nnaordex  8566  wdom2d  9485  iundom2g  10450  fzospliti  13607  rexuz3  15272  qredeq  16584  prmdvdsfz  16632  dirge  18526  lssssr  20905  lpigen  21290  psgnodpm  21543  psdmul  22109  neiptopnei  23076  metustexhalf  24500  dyadmbllem  25556  3cyclfrgrrn2  30362  atexch  32456  ordtconnlem1  34081  bj-ideqg1  37369  bj-imdirval3  37389  isbasisrelowllem1  37560  isbasisrelowllem2  37561  pibt2  37622  phpreu  37805  poimirlem26  37847  sstotbnd3  37977  eqlkr3  39361  dihatexv  41598  dvh3dim2  41708  unitscyglem4  42452  prjspner1  42869  oasubex  43528  naddwordnexlem4  43643  neik0pk1imk0  44288  pm14.123b  44667  ordpss  44691  climreeq  45859  uspgrlimlem1  48234  itscnhlc0xyqsol  49011