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  3826  reuan  3859  2reu1  3860  reupick  4292  reusv2lem3  5355  axprlem4  5381  ssrelrn  5858  relssres  5993  funmo  6531  funmoOLD  6532  funssres  6560  dffo4  7075  dffo5  7076  dfwe2  7750  ordpwsuc  7790  ordunisuc2  7820  dfom2  7844  nnsuc  7860  nnaordex  8602  wdom2d  9533  iundom2g  10493  fzospliti  13652  rexuz3  15315  qredeq  16627  prmdvdsfz  16675  dirge  18562  lssssr  20860  lpigen  21245  psgnodpm  21497  psdmul  22053  neiptopnei  23019  metustexhalf  24444  dyadmbllem  25500  3cyclfrgrrn2  30216  atexch  32310  ordtconnlem1  33914  bj-ideqg1  37152  bj-imdirval3  37172  isbasisrelowllem1  37343  isbasisrelowllem2  37344  pibt2  37405  phpreu  37598  poimirlem26  37640  sstotbnd3  37770  eqlkr3  39094  dihatexv  41332  dvh3dim2  41442  unitscyglem4  42186  prjspner1  42614  oasubex  43275  naddwordnexlem4  43390  neik0pk1imk0  44036  pm14.123b  44415  ordpss  44440  climreeq  45611  uspgrlimlem1  47987  itscnhlc0xyqsol  48754