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  2026  sbcg  3869  reuan  3904  2reu1  3905  reupick  4334  reusv2lem3  5405  axprlem4  5431  ssrelrn  5907  relssres  6041  funmo  6582  funmoOLD  6583  funssres  6611  dffo4  7122  dffo5  7123  dfwe2  7792  ordpwsuc  7834  ordunisuc2  7864  dfom2  7888  nnsuc  7904  nnaordex  8674  wdom2d  9617  iundom2g  10577  fzospliti  13727  rexuz3  15383  qredeq  16690  prmdvdsfz  16738  dirge  18660  lssssr  20969  lpigen  21362  psgnodpm  21623  psdmul  22187  neiptopnei  23155  metustexhalf  24584  dyadmbllem  25647  3cyclfrgrrn2  30315  atexch  32409  ordtconnlem1  33884  bj-ideqg1  37146  bj-imdirval3  37166  isbasisrelowllem1  37337  isbasisrelowllem2  37338  pibt2  37399  phpreu  37590  poimirlem26  37632  sstotbnd3  37762  eqlkr3  39082  dihatexv  41320  dvh3dim2  41430  unitscyglem4  42179  prjspner1  42612  oasubex  43275  naddwordnexlem4  43390  neik0pk1imk0  44036  pm14.123b  44421  ordpss  44446  climreeq  45568  uspgrlimlem1  47890  itscnhlc0xyqsol  48614