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  2032  sbcg  3801  reuan  3834  2reu1  3835  reupick  4269  reusv2lem3  5342  axprlem4  5368  ssrelrn  5849  relssres  5987  funmo  6514  funssres  6542  dffo4  7055  dffo5  7056  dfwe2  7728  ordpwsuc  7766  ordunisuc2  7795  dfom2  7819  nnsuc  7835  nnaordex  8574  wdom2d  9495  iundom2g  10462  fzospliti  13646  rexuz3  15311  qredeq  16626  prmdvdsfz  16675  dirge  18569  lssssr  20949  lpigen  21333  psgnodpm  21568  psdmul  22132  neiptopnei  23097  metustexhalf  24521  dyadmbllem  25566  3cyclfrgrrn2  30357  atexch  32452  ordtconnlem1  34068  bj-ideqg1  37478  bj-imdirval3  37498  isbasisrelowllem1  37671  isbasisrelowllem2  37672  pibt2  37733  phpreu  37925  poimirlem26  37967  sstotbnd3  38097  eqlkr3  39547  dihatexv  41784  dvh3dim2  41894  unitscyglem4  42637  prjspner1  43059  oasubex  43714  naddwordnexlem4  43829  neik0pk1imk0  44474  pm14.123b  44853  ordpss  44877  climreeq  46043  uspgrlimlem1  48464  itscnhlc0xyqsol  49241