Theorem ancrd 556

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  impac  557  equvinva  2037  sbcg  3795  reuan  3828  2reu1  3829  reupick  4257  reusv2lem3  5329  axprlem4  5355  ssrelrn  5836  relssres  5974  funmo  6501  funssres  6529  dffo4  7044  dffo5  7045  dfwe2  7717  ordpwsuc  7755  ordunisuc2  7784  dfom2  7808  nnsuc  7824  nnaordex  8564  wdom2d  9485  iundom2g  10453  fzospliti  13637  rexuz3  15302  qredeq  16617  prmdvdsfz  16666  dirge  18560  lssssr  20944  lpigen  21328  psgnodpm  21563  psdmul  22154  neiptopnei  23115  metustexhalf  24539  dyadmbllem  25584  3cyclfrgrrn2  30375  atexch  32470  ordtconnlem1  34108  bj-ideqg1  37524  bj-imdirval3  37544  isbasisrelowllem1  37717  isbasisrelowllem2  37718  pibt2  37779  phpreu  37971  poimirlem26  38013  sstotbnd3  38143  eqlkr3  39593  dihatexv  41830  dvh3dim2  41940  unitscyglem4  42683  prjspner1  43076  oasubex  43731  naddwordnexlem4  43846  neik0pk1imk0  44491  pm14.123b  44870  ordpss  44894  climreeq  46058  uspgrlimlem1  48479  itscnhlc0xyqsol  49256