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  2029  sbcg  3838  reuan  3871  2reu1  3872  reupick  4304  reusv2lem3  5370  axprlem4  5396  ssrelrn  5874  relssres  6009  funmo  6550  funmoOLD  6551  funssres  6579  dffo4  7092  dffo5  7093  dfwe2  7766  ordpwsuc  7807  ordunisuc2  7837  dfom2  7861  nnsuc  7877  nnaordex  8648  wdom2d  9592  iundom2g  10552  fzospliti  13706  rexuz3  15365  qredeq  16674  prmdvdsfz  16722  dirge  18611  lssssr  20909  lpigen  21294  psgnodpm  21546  psdmul  22102  neiptopnei  23068  metustexhalf  24493  dyadmbllem  25550  3cyclfrgrrn2  30214  atexch  32308  ordtconnlem1  33901  bj-ideqg1  37128  bj-imdirval3  37148  isbasisrelowllem1  37319  isbasisrelowllem2  37320  pibt2  37381  phpreu  37574  poimirlem26  37616  sstotbnd3  37746  eqlkr3  39065  dihatexv  41303  dvh3dim2  41413  unitscyglem4  42157  prjspner1  42596  oasubex  43257  naddwordnexlem4  43372  neik0pk1imk0  44018  pm14.123b  44398  ordpss  44423  climreeq  45590  uspgrlimlem1  47948  itscnhlc0xyqsol  48693