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  3863  reuan  3896  2reu1  3897  reupick  4329  reusv2lem3  5400  axprlem4  5426  ssrelrn  5905  relssres  6040  funmo  6581  funmoOLD  6582  funssres  6610  dffo4  7123  dffo5  7124  dfwe2  7794  ordpwsuc  7835  ordunisuc2  7865  dfom2  7889  nnsuc  7905  nnaordex  8676  wdom2d  9620  iundom2g  10580  fzospliti  13731  rexuz3  15387  qredeq  16694  prmdvdsfz  16742  dirge  18648  lssssr  20952  lpigen  21345  psgnodpm  21606  psdmul  22170  neiptopnei  23140  metustexhalf  24569  dyadmbllem  25634  3cyclfrgrrn2  30306  atexch  32400  ordtconnlem1  33923  bj-ideqg1  37165  bj-imdirval3  37185  isbasisrelowllem1  37356  isbasisrelowllem2  37357  pibt2  37418  phpreu  37611  poimirlem26  37653  sstotbnd3  37783  eqlkr3  39102  dihatexv  41340  dvh3dim2  41450  unitscyglem4  42199  prjspner1  42636  oasubex  43299  naddwordnexlem4  43414  neik0pk1imk0  44060  pm14.123b  44445  ordpss  44470  climreeq  45628  uspgrlimlem1  47955  itscnhlc0xyqsol  48686