Theorem ancrd 555

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 516	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜓)))

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  impac  556  equvinva  2038  sbcg  3774  reuan  3808  2reu1  3809  reupick  4233  reusv2lem3  5293  ssrelrn  5763  relssres  5892  funmo  6396  funssres  6424  dffo4  6922  dffo5  6923  dfwe2  7559  ordpwsuc  7594  ordunisuc2  7623  dfom2  7646  nnsuc  7662  nnaordex  8366  wdom2d  9196  iundom2g  10154  fzospliti  13274  rexuz3  14912  qredeq  16214  prmdvdsfz  16262  dirge  18109  lssssr  19990  lpigen  20294  psgnodpm  20550  neiptopnei  22029  metustexhalf  23454  dyadmbllem  24496  3cyclfrgrrn2  28370  atexch  30462  ordtconnlem1  31588  bj-ideqg1  35070  bj-imdirval3  35090  isbasisrelowllem1  35263  isbasisrelowllem2  35264  pibt2  35325  phpreu  35498  poimirlem26  35540  sstotbnd3  35671  eqlkr3  36852  dihatexv  39089  dvh3dim2  39199  prjspner1  40171  neik0pk1imk0  41334  pm14.123b  41717  ordpss  41742  climreeq  42829  itscnhlc0xyqsol  45784