Theorem ancrd 554

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  impac  555  equvinva  2036  reuan  3883  2reu1  3884  reupick  4290  reusv2lem3  5304  ssrelrn  5766  relssres  5896  funmo  6374  funssres  6401  dffo4  6872  dffo5  6873  dfwe2  7499  ordpwsuc  7533  ordunisuc2  7562  dfom2  7585  nnsuc  7600  nnaordex  8267  wdom2d  9047  iundom2g  9965  fzospliti  13072  rexuz3  14711  qredeq  16004  prmdvdsfz  16052  dirge  17850  lssssr  19728  lpigen  20032  psgnodpm  20735  neiptopnei  21743  metustexhalf  23169  dyadmbllem  24203  3cyclfrgrrn2  28069  atexch  30161  ordtconnlem1  31171  bj-ideqg1  34460  bj-imdirval3  34478  bj-imdirid  34479  isbasisrelowllem1  34640  isbasisrelowllem2  34641  pibt2  34702  phpreu  34880  poimirlem26  34922  sstotbnd3  35058  eqlkr3  36241  dihatexv  38478  dvh3dim2  38588  neik0pk1imk0  40403  pm14.123b  40764  ordpss  40789  climreeq  41900  itscnhlc0xyqsol  44759