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  2030  sbcg  3829  reuan  3862  2reu1  3863  reupick  4295  reusv2lem3  5358  axprlem4  5384  ssrelrn  5861  relssres  5996  funmo  6534  funmoOLD  6535  funssres  6563  dffo4  7078  dffo5  7079  dfwe2  7753  ordpwsuc  7793  ordunisuc2  7823  dfom2  7847  nnsuc  7863  nnaordex  8605  wdom2d  9540  iundom2g  10500  fzospliti  13659  rexuz3  15322  qredeq  16634  prmdvdsfz  16682  dirge  18569  lssssr  20867  lpigen  21252  psgnodpm  21504  psdmul  22060  neiptopnei  23026  metustexhalf  24451  dyadmbllem  25507  3cyclfrgrrn2  30223  atexch  32317  ordtconnlem1  33921  bj-ideqg1  37159  bj-imdirval3  37179  isbasisrelowllem1  37350  isbasisrelowllem2  37351  pibt2  37412  phpreu  37605  poimirlem26  37647  sstotbnd3  37777  eqlkr3  39101  dihatexv  41339  dvh3dim2  41449  unitscyglem4  42193  prjspner1  42621  oasubex  43282  naddwordnexlem4  43397  neik0pk1imk0  44043  pm14.123b  44422  ordpss  44447  climreeq  45618  uspgrlimlem1  47991  itscnhlc0xyqsol  48758