Theorem ancrd 578

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 556	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 197  df-an 385

This theorem is referenced by:  impac  652  equviniva  2101  reupick  4042  prel12OLD  4515  reusv2lem3  5008  ssrelrn  5458  ssrnres  5718  funmo  6053  funssres  6079  dffo4  6526  dffo5  6527  dfwe2  7134  ordpwsuc  7168  ordunisuc2  7197  dfom2  7220  nnsuc  7235  nnaordex  7875  wdom2d  8638  iundom2g  9525  fzospliti  12665  rexuz3  14258  qredeq  15544  prmdvdsfz  15590  dirge  17409  lssssr  19126  lpigen  19429  psgnodpm  20107  neiptopnei  21109  metustexhalf  22533  dyadmbllem  23538  3cyclfrgrrn2  27412  atexch  29520  ordtconnlem1  30250  isbasisrelowllem1  33485  isbasisrelowllem2  33486  phpreu  33675  poimirlem26  33717  sstotbnd3  33857  eqlkr3  34860  dihatexv  37098  dvh3dim2  37208  neik0pk1imk0  38816  pm14.123b  39098  ordpss  39126  climreeq  40317  reuan  41655  2reu1  41661