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  3815  reuan  3848  2reu1  3849  reupick  4283  reusv2lem3  5347  axprlem4  5373  ssrelrn  5851  relssres  5989  funmo  6516  funssres  6544  dffo4  7057  dffo5  7058  dfwe2  7729  ordpwsuc  7767  ordunisuc2  7796  dfom2  7820  nnsuc  7836  nnaordex  8576  wdom2d  9497  iundom2g  10462  fzospliti  13619  rexuz3  15284  qredeq  16596  prmdvdsfz  16644  dirge  18538  lssssr  20917  lpigen  21302  psgnodpm  21555  psdmul  22121  neiptopnei  23088  metustexhalf  24512  dyadmbllem  25568  3cyclfrgrrn2  30374  atexch  32469  ordtconnlem1  34102  bj-ideqg1  37419  bj-imdirval3  37439  isbasisrelowllem1  37610  isbasisrelowllem2  37611  pibt2  37672  phpreu  37855  poimirlem26  37897  sstotbnd3  38027  eqlkr3  39477  dihatexv  41714  dvh3dim2  41824  unitscyglem4  42568  prjspner1  42984  oasubex  43643  naddwordnexlem4  43758  neik0pk1imk0  44403  pm14.123b  44782  ordpss  44806  climreeq  45973  uspgrlimlem1  48348  itscnhlc0xyqsol  49125