Theorem ancrd 575

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  impac  649  equviniva  1947  reupick  3870  prel12  4323  reusv2lem3  4797  ssrelrn  5237  ssrnres  5491  funmo  5820  funssres  5844  dffo4  6283  dffo5  6284  dfwe2  6873  ordpwsuc  6907  ordunisuc2  6936  dfom2  6959  nnsuc  6974  nnaordex  7605  wdom2d  8368  iundom2g  9241  fzospliti  12369  rexuz3  13936  qredeq  15209  prmdvdsfz  15255  dirge  17060  lssssr  18774  lpigen  19077  psgnodpm  19753  neiptopnei  20746  metustexhalf  22171  dyadmbllem  23173  3cyclfrgrarn2  26541  atexch  28624  ordtconlem1  29298  isbasisrelowllem1  32379  isbasisrelowllem2  32380  phpreu  32563  poimirlem26  32605  sstotbnd3  32745  eqlkr3  33406  dihatexv  35645  dvh3dim2  35755  neik0pk1imk0  37365  pm14.123b  37649  ordpss  37676  climreeq  38680  reuan  39829  2reu1  39835  3cyclfrgrrn2  41457