Theorem ancrd 552

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  impac  553  equvinva  2014  reuan  3808  2reu1  3809  reupick  4207  reusv2lem3  5192  ssrelrn  5649  relssres  5774  funmo  6241  funssres  6268  dffo4  6732  dffo5  6733  dfwe2  7352  ordpwsuc  7386  ordunisuc2  7415  dfom2  7438  nnsuc  7453  nnaordex  8114  wdom2d  8890  iundom2g  9808  fzospliti  12919  rexuz3  14542  qredeq  15830  prmdvdsfz  15878  dirge  17676  lssssr  19415  lpigen  19718  psgnodpm  20414  neiptopnei  21424  metustexhalf  22849  dyadmbllem  23883  3cyclfrgrrn2  27758  atexch  29849  ordtconnlem1  30784  isbasisrelowllem1  34167  isbasisrelowllem2  34168  pibt2  34229  phpreu  34407  poimirlem26  34449  sstotbnd3  34586  eqlkr3  35768  dihatexv  38005  dvh3dim2  38115  neik0pk1imk0  39882  pm14.123b  40296  ordpss  40322  climreeq  41436  itscnhlc0xyqsol  44233